IF Frequently Asked Questions

Q1: How to analyze IF specifications ?
Q2: ...

Q1. How to analyze IF specifications ?

You must follow the following steps:
  1. Build the simulator
  2. Explore the model
  3. Build the model
  4. Optimize

1. Build the simulator

In order to build the simulator for an IF specification, let's say token.if, execute the following command:
$ make -f $IF/examples/Makefile token.x
The simulator will be constructed as an executable file called token.x.

2. Explore the model

If the construction of the simulator succeeds, you may run the simulator interactively: 
$ token.x -inter
Or, you can also try the random mode: 
$ token.x -random

3. Build the model

With the following command: 
$ token.x [-bfs|-dfs] [-po]
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 order reduction.

If you run the simulator with the following command:
$ token.x -bfs -t token.aut -q token.states

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 system states.

4. Optimize

If the model is too big, you can optimize the specification  using live variable analysis. The following command: 
$ dfa -live token.if > token.live.if

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.