Update Released (0.3)

New Version Released (0.3)

Synchronization Skeleton for Mutex of 3 processes with shared variables to keep track of priority.

New Features:

 - Decision Procedure: The tool provides an Implementation of the Decision Procedure [Emerson and Clark 82]. The decision procedure is accessed from the tools menu, it can be used to determine the satiability or validity of boolean formulae, the tableau (before deletions) can also be displayed.

 - Concurrent Abstraction: Concurrent Kripke Structures can be abstracted efficiently (By labels or sub-formulae). The concertized repair is model checked against the original specifications, as well as checked for synchronization between the pairs.

 - Synchronization Skeleton: Kripke Structures (single and concurrent) can now be transformed to a synchronization skeleton. Synchronization Skeleton can be edited by adding or removing states and transitions. Synchronization Skeletons can be transformed back to Kripke Structures.

Downloads:

 - The new version of the tool (version 0.3) can be downloaded here. It is a runnable jar file, it required java 7. Please notice that the tool is still under development and is not a final-release.

Tableau for determining satisfiability of [ AX(P) & P => AG(P) ]

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.