A model-checker for LTL properties built using libITS.

its-ltl

What is its-ltl

its-ctl is our model-checker for Linear-time Temporal Logic properties, built upon libITS and Spot. It offers support for efficient symbolic CTL model checking using saturation and forward transition relation among other features.

its-ltl is a library and tool for LTL model-checking of Instantiable Transition Systems. It leverages on the ITS and SDD libraries and on the model-checking library Spot which handles translation of LTL formulae to TGBA a variant of Buchi automata. Spot does not compile easily on cygwin platform, so this tool is only available for linux and macosX. Features:

  • ITS model input: any ITS model can be LTL checked.
  • Two algorithms adapted to stuttering invariant properties for hybrid explicit/symbolic LTL\X model checking. Option -SSOG implements the Symbolic Observation Graph approach, and -SSOP is a new more efficient dynamic version of the same.
  • One algorithm for hybrid explicit/symbolic full LTL model checking. Option -SSLAP implements a novel approach: the Symbolic Local Aggregation Product.
  • Fully symbolic LTL checking using forward OWCTY or EL algorithms.

Obtaining its-ltl

You can download the current release as well as binaries from here: ITS-LTL download page

The latest source version of its-ltl can be obtained from GitHub at https://github.com/lip6/ITS-LTL.

Note that to build from the git, you need autotools and to invoke “autoreconf -vfi” to create the “configure” script. Due to various dependencies, building from git requires some configuration settings.

Remember, configure –help is your friend, and you can also have a look at the configuration settings of our Travis continuous integration server or AppVeyor for Windows for inspiration on how to invoke configure.

The only dependencies are libDDD, libITS and Spot that you need to deploy first.

Usage

If you just intend to use the tool at a command-line, run it with option “-h” to get a description of various options available.

The Samples/ folder contains many examples, and the tests/ folder cover many common invocation idioms. Note that the command-line tool is meant for experts or back-end model-checking, and it is usually invoked through scripts on verified input or as generated by other tools.

If you want to experiment using the command line tool on models edited with ITS modeler front-end, just run any analysis on your model, a side effect is to generate input compatible with the command line tool in the current “work” folder.

See this page for invocation examples.

You can also use the eclipse front-end to produce valid command line invocations of its-ltl.

Checking LTL properties

To verify LTL properties use flag “-ltl LTLFILE” and pass a file containing LTL formulas. See the “tests/” folder for examples of legal LTL files.

  • the page choosing an algorithm explains the ideas behind the flags
  • TODO : we should really document the options more throughly. Please read the help at bottom of this page or contact us ddd@lip6.fr if you have trouble running the tool

Acknowledgement

The code base for its-ltl is loosely based on the tool checksog by Denis Poitrenaud and Kais Klai. Most of the current code base is due to Alexandre Duret-Lutz, Denis Poitrenaud, Yann Thierry-Mieg, and Kais Klai.

Improvements and the new SCC decomposition based method were provided as patches by Etienne Renault.

Maximilien Colange also contributed improvements to handling of Divine atomic propositions.

Ala Eddine Bensalem contributed the whole TGTA functionality and algorithm.

For further credits and version history please browse the repository history.

its-ltl –help

Instantiable Transition Systems SDD/DDD Analyzer; package ITSREACH 0.2

This tool performs state-space analysis of Instantiable Transition Systems a.k.a. ITS

The reachability set is computed using SDD/DDD of libDDD, the Hierarchical Set Decision Diagram library,

MANDATORY Options :

  • -i path : specifies the path to input model file
  • -t {CAMI,PROD,ROMEO,ITSXML,ETF,DLL,NDLL,DVE,GAL,CGAL} : specifies format of the input model file : * CAMI : CAMI format (for P/T nets) is the native Petri net format of CPN-AMI * PROD : PROD format (for P/T nets) is the native format of PROD * ROMEO : an XML format (for Time Petri nets) that is the native format of Romeo * UROMEO : Romeo format with additional constraints: all places named, with different names. * ITSXML : a native XML format (for ANY kind of ITS) for this tool. These files allow to point to other files. * ETF : Extended Table Format is the native format used by LTSmin, built from many front-ends. * DLL : use a dynamic library that provides a function “void loadModel (Model &,int)” typically written using the manipulation APIs. See demo/ folder. * NDLL : same as DLL, but expect input formatted as size:lib.so. See demo/ folder. * DVE : Divine is a modelling language similar to Promela. * GAL : Guarded Action Language. * CGAL : Guarded Action Language + Composite/ITS textual syntax. File must contain a main declaration.

Additional Options and Settings:

  • –trace-states : if set, this option will force to print intermediate states (up to print limit) when showing traces.
  • –print-limit INT : set the threshold for full printout of states in traces. DD holding more states than threshold will not be printed. [DEFAULT:10 states]
  • –load-order path : load the variable order from the file designated by path. This order file can be produced with –dump-order. Note this option is not exclusive of –json-order; the model is loaded as usual, then the provided order is applied a posteriori.

Petri net specific options :

  • –json-order path : use a JSON encoded hierarchy description file for a Petri net model (CAMI, PROD or ROMEO), such as produced using Neoppod heuristic ordering tools. Note that this option modifies the way the model is loaded.

  • –sdd : privilege SDD storage (Petri net models only).(DEFAULT)
  • –ddd : privilege DDD (no hierarchy) encoding (Petri net models only).

Scalar and Circular symmetric composite types options:

  • -ssD2 INT : (depth 2 levels) use 2 level depth for scalar sets. Integer provided defines level 2 block size. [DEFAULT: -ssD2 1]
  • -ssDR INT : (depth recursive) use recursive encoding for scalar sets. Integer provided defines number of blocks at highest levels.
  • -ssDS INT : (depth shallow recursive) use alternative recursive encoding for scalar sets. Integer provided defines number of blocks at lowest level.

GAL-based specific options (DVE and GAL):

  • –gen-order STRAT : Invoke ordering heuristic to compute a static ordering. STRAT should be one of the following [default DEFAULT]:
    • DEFAULT : historical strategy, does not follow labels of ‘call’ statements
    • FOLLOW : follows the labels of ‘call’ statements
    • FOLLOW_HALF : follows the labels of ‘call’ statements, but with halved weight
    • FOLLOW_DOUBLE : follows the labels of ‘call’ statements, but with doubled weight
    • FOLLOW_SQUARE : same as FOLLOW, but uses energy-based costs
    • FOLLOW_DYN : follows the labels of ‘call’ statements, with a cost related to constraint’ size
    • FOLLOW_DYN_SQ : same as FOLLOW_DYN, but uses energy-based costs
    • FOLLOW_FDYN : same as FOLLOW_DYN, but the cost is related to the size for all constraints (even with no ‘call’)
    • FOLLOW_FDYN_SQ : same as FOLLOW_FDYN, but uses energy-based costs
    • LEXICO : use the old strategy, based on lexicographical ordering of the variable

SDD specific options :

  • –no-garbage : disable garbage collection (may be faster, more memory)
  • –gc-threshold INT : set the threshold for first starting to do gc [DEFAULT:13000 kB=1.3GB]
  • –fixpoint {BFS,DFS} : this options controls which kind of saturation algorithm is applied. Both are variants of saturation not really full DFS or BFS. [default: BFS]

This tool performs LTL verification on state-space of ITS LTL specific options for package SOGITS 0.1

MANDATORY : specify a formula to check

  • -LTL formula_file formula read from formula_file, one per line, lines starting with # are ignored.
  • -ltl formula specify the ltl formula as a string. Must be stuttering invariant for SOG and SOP variants.

Actions:

  • -aALGO apply the emptiness check algoritm ALGO
  • -SSOGTYPE apply the SOG construction algoritm SOGTYPE={SOG,SLAP,SOP,FSOWCTY,FSOWCTY-TGTA,FSEL,BCZ99,SLAP-FST,SLAP-FSA} (SLAP-FST by default)
    • The FST variants include a test for switching to fully symbolic emptiness check in terminal states.
    • The FSA variants include a test for switching to fully symbolic emptiness check in any potentially accepting automaton state.
  • –place-syntax suppose that atomic properties are just names of variables: “Idle” will be interpreted as “Idle=1”
  • -C display the number of states and edges of the SOG
  • -c check the formula

  • -e display a sequence (if any) of the net satisfying the formula (implies -c)

  • -g display the sog
  • -p display the net
  • -s show the formula automaton
  • -stutter-deadlock stutter in deadlock states

Options of the formula transformation:

  • -dR3 disable the SCC reduction
  • -R3f enable full SCC reduction
  • -b branching postponement (false by default)
  • -l fair-loop approximation (false by default)
  • -x try to produce a more deterministic automaton (false by default)
  • -y do not merge states with same symbolic representation (true by default)

Where ALGO should be one of:

  • Cou99(OPTIONS) (the default)
  • CVWY90(OPTIONS)
  • GV04(OPTIONS)
  • SE05(OPTIONS)
  • Tau03(OPTIONS)
  • Tau03_opt(OPTIONS)
Tags: