New Version Released (0.4)
New Features:  |
| Actions in a colored Kripke Structure |
 |
| Global Model Check |
 |
| Refinements |
 |
| Synchronization Skeletons Editor |
 |
| Scripting REPL |
- Action Synchronization: You can now synchronize transition shared between multiple processes using action names. You can choose whether to use synchronization by process indices, by action names, or both when repairing the structure. Actions are supported by all the other features (abstractions, transforming to synchronization skeletons, etc ...).
- Global Model Checking: Eshmun can check whether any user-provided CTL formula holds at state. States that satisfy the formula will be shaded in grey, other states will be displayed as usual. This process is similar to model checking the structure many times, each time using one of the states as a start state.
- Unsat Core: If the structure is unrepairable, you can use a minimal unsat core to determine a small subset of states and transitions that are causing the structure to be unrepairable. At least one start state will be part of this set. Eshmun will communicate with the Unsat core solver and highlight the subset graphically. This feature requires you to get MUSer2. When using this feature Eshmun will look for MUSer2 in the same directory, if it fails to find it, it will prompt a dialog box asking for its location. You can get MUSer2 from http://logos.ucd.ie/web/doku.php?id=muser .
- Synchronization Skeletons Editor: Eshmun's Synchronization Skeletons editor is now enhanced, it is easier to input/modify the guards, as well as add additional states and transitions to the skeletons. The guards can refer to action names.
- Scripting: Eshmun provides a built in small scripting language for creating structures quickly. You can use the scripting language to quickly replicate an existing structure, modify existing ones, or create them from scratch. The scripting language contains loops and conditionals that can be used to determine which pairs of processes to create. It also contains constructs to import/load structures from Eshmun. The scripts can be written in a file or directly into a REPL Terminal inside Eshmun.
- Refinements: Repair of big or complicated structures is often an iterative process, that includes modifying the structure and specifications, iteratively repairing the structure against different specifications, and using other helpful features of Eshmun (transforming to skeletons, abstractions, etc..). Eshmun supports recording these different steps to track the different stages of repair. The resulting sequences of steps (a refinement) can be saved, loaded, and modified.
- Visual Aids: Additional visual aids have been added to Eshmun. This facilitates navigating and understanding big structures. These aids include custom coloring of actions, labels, and transitions based on the process they belong to or the action name they synchronize by, determining which process to show and which hide, as well as displaying different statistics about the size of the structures, repairs, and internal SAT formulae.
User Help: Please refer to the user manual inside Eshmun (in the help menu) for a detailed user manual. The manual covers all the existing features, and provides helpful tips on how to use Eshmun in general.
Backwards Compatibility:
- Saved structures from older versions may not work. Depending on what features are used in these saved structures, the new version may fail to open them. This issue can be solved by using an older version of Eshmun to export these structures into text format, then importing the text format into the new version of Eshmun. The imported structures will be automatically "upgraded", and can be dealt with as if structures produced by the new version.
Downloads:
- The new version of the tool (version 0.4) can be downloaded here. It is a runnable jar file, it is recommended to use Java 8, but java 7 is also supported. Please notice that the tool is still under development and is not a final-release.
Bug reports:
If a bug was encountered, please submit a bug report to the following email eshmuntool@gmail.com, please attach with it a saved copy of the structure causing the bug, or details on how to reproduce the bug on our machines to study it. Your feedback is highly appreciated and will help us deliver a better tool.
