The following zip file contains the CLTSA java executable file (.jar)
Roadmap
- Conditional Counting Fluents: feature that can yield the counting fluent behavior to some propositional C fluent state, i.e. when C is false the regarded counting fluent remains frozen.
- Counting Fluent indexation and Counting Fluent array's arithmetical operations such as SUM.
Release history
07-03-2016
New features
New features
bug fixed
New features
New features
New features
New features
- Minor improvements: Shortcuts was added for common commands (open, save, copy, cut, paste, undo, redo, compile).
New features
- LTSA-Delforge extensive LTS layout capabilities merged into CLTSA. Thanks to Cédric Delforge, Charles Pecheur!.
bug fixed
- Negative integer values allowed in limits definitions
New features
- Non-Strict limit for counting fluent analysis support. On these configurations for c.fluents, the possible analysis outputs are:
- Valid (no counterexample found and no c.fluent limits violation was reached)
- False (a valid counterexample was found)
- may be (no counterexample found but c.fluent limits violation was reached)
New features
- Counting fluents and counting expression support
- New syntax definition with optional limit definition ( old version as bounds and scopes )
- cassert keyword moved to standard assert definition and any LTL formula support.
- Counting expressions (arithmetic inequalities at LTL formula) with multiple counting fluents support
- New Büchi Automata based Model checking algorithm (transparent to the user)
- Counterexample fluents information trace improved in the output analysis result
- Configurable fluents report at the System Animator
- Examples incorporated into the examples menu
New features
- Counting fluents and counting expression support
- Model Checking support (Monitor and synchronization FSP process generation)
