How to use CISMO
 

The options are divided as follow in the menu :

File

System

Create a new model
Creates a new model from a simple wizard.

Verify LMP constraints
This function verifies that the model respects the labelled Markov chains constraints. These contraints are as follow :
1. The state space must be a subset of the real numbers.
2. Every interval of the X states set must be disjoint.
3. Every interval of the Y states set must be disjoint.
4. The model must possess an initial state.
5. Every action must be identified with a string. If two string are equivalent, then they represent the same action.
6. For every state and for every action, the probability to reach any action must higher or equal to zero and lower or equal to one.
7. A transition must be defined for a continuous starting state set, a continuous destination state set and a specific action.

Generate a random system
This is very useful for testing and benchmarking. It generates a random LMP system or a finite state space system. For more information, consult the model generator page.

Transitions

Create a new transition
Creates a transition using a simple wizard.

Modify a transition
Modify a transition using a simple wizard.

Remove a transition
Remove the transition from the list.

Formulas

Add a new formula
Verify a new formula using the currently loaded model. For more information, consult the formula editor page.

Modify a formula
Use an existing formula from the history to build a new formula. For more information, consult the formula editor page.

Remove a formula
Remove the selected formula from the history.

Options

Preferences
Set the general CISMO preferences. For more information, consult the CISMO options page.

Also note that double-clicking on the transition list is equivalent to "modify a transition", and double-clicking on the formula history is equivalent to "modify a formula".