IF Frequently Asked Questions
Q1: How to analyze IF specifications ?
Q1. How to analyze IF specifications ?
You must follow the following steps:
- Build the simulator
- Explore the model
- Build the model
1. Build the simulator
In order to build the simulator for an IF specification, let's say token.if, execute the following command:
The simulator will be constructed as an executable file called token.x.
$ make -f $IF/examples/Makefile token.x
2. Explore the model
If the construction of the simulator succeeds, you may run the simulator
Or, you can also try the random mode:
$ token.x -inter
$ token.x -random
3. Build the model
With the following command:
the simulator will explore all the reachable states using a breadth-first
search (bfs) or depth-first search (dfs) strategy.
During the exploration it will print the number of the reached states
and transitions. In dfs mode, the -po option enables partial
$ token.x [-bfs|-dfs] [-po]
If you run the simulator with the following command:
it will create files token.aut (in Aldebaran format, see CADP web page for details)
containing the system behavior as a flat labeled transition
system, and token.states containing the description of the
$ token.x -bfs -t token.aut -q token.states
If the model is too big, you can optimize the specification using
live variable analysis. The following command:
will generate a new specification token.live.if, equivalent with
token.if up to the values of dead variables.
The corresponding model is usually much smaller.
$ dfa -live token.if > token.live.if