CLTSA:  LABELLED TRANSITION SYSTEM ANALYsER with COUNTING FLUENT support
  • Home
  • Model Checking
  • Examples
  • Demo & Benchmarks
  • Download
  • Publications
  • About
  • Contact
The following zip file contains the CLTSA java executable file (.jar)

Download

    Bug Reporting

Submit

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
  • Minor improvements:  Shortcuts was added for common commands (open, save, copy, cut, paste, undo, redo, compile). ​
​26-11-2015
​
New features
  • LTSA-Delforge extensive LTS layout capabilities merged into CLTSA. Thanks to Cédric Delforge, Charles Pecheur!.​
13-11-2015
bug fixed
  • Negative integer values allowed in limits definitions
05-11-2015
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)  ​
30-09-2015
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
20-10-2014
New features
  • Counting fluents and counting expression support
  • Model Checking support (Monitor and synchronization FSP process generation)
Powered by Create your own unique website with customizable templates.
  • Home
  • Model Checking
  • Examples
  • Demo & Benchmarks
  • Download
  • Publications
  • About
  • Contact