CISMO file format

In addition to using menus to build your system, or using the model generator, you can also edit your files by hand. The model files recognized by Cismo are plain text files respecting the following constraints :

1. All the intervals in Cismo are written in the following format :
    [a,b] if both bounds are inclusive.
    (a,b] if the lower bound is exclusive while the other is inclusive.
    [a,b) if the upper bound is exclusive while the other is inclusive.
    (a,b) if both bouns are exclusive.
    {a} if a represents a precise point.

2. Every line must end with a semicolon.

3. Respect the following structure :

states : <interval>
Represents the state space of the model. Every transitions must have its source and destination included in the state space.

init : <real number>
Represents the initial state of the model. This number must be included in the state space.

NbActions : <integer number>
Represents the number of actions that can be applied to the model.You must be careful not to define more actions than this number.

X : <list of intervals>
Represents all the intervals that can be a source of a transition. A list of intervals is in the format <interval> U <interval>.

Y : <list of intervals>
Represents all the intervals that can be the destination of a transition.

transition
This keyword marks the beginning of the transition list.

Each transition is in the following format :
<source>    -[<action>]-    <probabilistic formula> :    <destination> ;
example:
[47.91,63.33) -[action3]-> 0.4*(y/20.54): [0.0,20.54) ;

endtransition
Marks the end of the transition list. Failure to include this keyword will result in CISMO not accepting the file.