Ada - the arithmetic DDS analyzer

CTL* model checking with arithmetic

Help

Ada is a tool for model checking of data-aware dynamic systems with arithmetic (DDSAs) with respect to CTL*_f properties, i.e., linear- and branching-time properties with a finite-trace semantics.

Input

Example systems can be selected from the dropdown menu. Here we provide a brief description of its components.

DDSA

Ada uses a simple json format for DDSAs, according to either this json schema or data Petri nets (DPNs) as pnml. The json has to specify states, transitions (possibly with guards), and variables, as in the following example:

{  "name" : "my example",
   "states": [
     {
        "id": 0,
        "name": "b0",
        "initial": true
     },
     {
        "id": 1,
        "name": "b1",
        "final": true
     }
   ],
   "transitions": [
     {
        "source": 0,
        "target": 1,
        "name": "increment x",
        "guard": "(x' == x + 1)"
     },
     {
        "source": 1,
        "target": 0,
        "name": "reset x",
        "guard": "(x' > 0)"
     }
   ],
   "variables": [ 
      {
         "name": "x",
         "type": "int",
         "initial": 0
      }
   ]
}

Here the sources and targets of transitions refer to the numeral state ids. The names of states and transitions can be referred to in the CTL*_f formula, see below. For variables, besides a name also a type (int or rat or bool) must be specified, as well as an initial value. Guards in transitions are expected to be formulas written according to the grammar

guard ::= (atom) | guard && guard | (guard)
atom ::= term == term | term != term | term < term | term <= term
term ::= k | var | term + term | term - term
var ::= v | v'

where k is a number, and v is the name a variable in the DDSA. In a guard, an occurrence of v refers to the current value, i.e., the variable is read; while v' refers to its value in the next state, i.e., the variable is written.

Formula

The CTL*_f formula chi should adhere to the following grammar:

chi ::=
 E psi |
 A psi |
 ! chi |
 chi && chi |
 (chi)
psi ::= 
 atom | 
 psi && psi | 
 psi || psi | 
 X psi | 
 <a> psi | 
 F psi | 
 G psi | 
 psi U psi | 
 chi |
 (psi) 
atom ::= 
 b | 
 term == term | 
 term != term | 
 term < term | 
 term <= term
term ::= 
 k | 
 v | 
 term + term | 
 term - term

where k is a number, v is a variable in the DDSA, b is the name of a state in the DDSA, and a is the name of a transition (action) in the DDSA. The temporal operators are X (next), <a> (next via action a) F (future, ◊), and G (globally, ◻).

Functionality

The tool performs CTL*_fmodel checking. It outputs the configuration map, which gives conditions for every control state to satisfy the property. The tool also reports whether the initial state satisfies the property.

Top