Tutorial of fc2symbmin v1.3
Date: 1999/04
Author: Michel Bourdelles (mbourdel@sophia.inria.fr)
This is a tutorial for the fc2tool fc2symbmin specific
to automata obtained from esterel encodings defined with
no counters and no tests on data.
We suppose you dispose an esterel compiler, and one of
the ocfc2 or bliffc2 processor.
We ask you to take the atg fc2 automata visualisation
environment.
This fc2symbmin processor allows the following functionnalities:
These tools take as input a fc2 automaton and
print a fc2 automaton or computation information.
-
Minimisation
- a simple example
- a second example
A simple example
This first example we propose to study has
been encoded by Amar Bouali and Robert de Simone
(reference ).
It is a synchronous token ring with four cells
which can take the token, just one cell at the
same time.
You will find it at ../Arbiter/arbiter.strl
Generating a fc2 file (prev, next)
This controller is causal under the constructive causality,
not under the causality of esterelv3 or topological sort
of esterelv4. You need an esterel compiler version
greater or equal than esterelv5_01 to compile it. If you have
not, you can directly work on the oc and blif files obtained.
There are many ways to obtain the corresponding fc2 automaton
file.
- esterel -oc -causal arbiter.strl
ocfc2 arbiter.oc
- esterel -Lblif -causal arbiter.strl
bliffc2 -fc2 arbiter.blif
minimisation (prev, next)
you minimise the fc2 automaton with the following command
fc2symbmin ocfc2_out.Arbiter4.fc2 > redArbiter.fc2
--- fc2parser: parsing ocfc2_out.Arbiter4.fc2
--- fc2parser: ocfc2_out.Arbiter4.fc2 parsed
--- fc2symbmin: Automaton has 6 vertice, 96 transitions
--- fc2min: block 4
--- fc2symbmin: Automaton has 4 states, 4 transitions
visualisation (prev, next)
You see the automaton obtained with Autograph by
the following command:
atg redArbiter.fc2
A second example (prev, next)
The second example is an interface communication with a Pump
controler. This pump controller has a physical controller
called pump which indicates if the pump is opened or closed,
and an other controller called ctl_Pump which store the order
send to the pump.
>
The pump takes one instant to open after an open_pump_command
and Close immediately after a close_pump_command.
Each instant, the pump sends his status (signals pump and
pump_ctl). If this status does not correspond to what it
is supposed to be, a protocol is executed until the pump
is repaired (module Problem).
The esterel encoding is in ./Pump/One_pump.strl
Generating a fc2 file (prev, next)
You can obtain the fc2 automaton with the following
commands.
A- esterel -oc One_pump.strl
ocfc2 One_pump.oc
B- esterel -Lblif One_pump.strl
bliffc2 -fc2 One_pump.blif
minimisation (prev, next)
fc2symbmin One_pump.Pump.fc2
--- fc2parser: parsing One_pump.Pump.fc2
--- fc2parser: One_pump.Pump.fc2 parsed
--- fc2symbmin: Automaton has 61 vertice, 2216 transitions
--- fc2min: block 11
--- fc2symbmin: Automaton has 11 states, 45 transitions
Observation by side programs
In the directory ./Arbiter/. ,few observers are described as
the esterel encodings.
Safety properties
The observer may simulate the environment of the controller
to check and indicates if a behavior is realized by the
controller in emitting a specific signal of success or
failure.
In obs1.strl, it indicates property signal
AT_MOST_ONE_ACK_Violated is emitted
if two Acknowledgment are emitted instantaneously
In obs2.strl, it indicates property signal
AT_LEAST_ONE_ACK_VIOLATED is emitted
if no instantaneous Acknowledgment is emitted
in case of request.
In obs3.strl, it indicates property signal
ACK_Without_Req_Violated is emitted
if an Acknowledgment is emitted for a cell with the request
not present (not emitted by the program) in the instant.
Liveness properties
In obs4.strl, it indicates property signal
if a cell requests a cell in all the instant, it will obtain
the acknowlegment.
The -restrict option indicates signals can just be emitted by the program
to verify.
Checking safety properties
We check the properties in applying the following
commands.
the -restrict option restrict the observer input signals to
be emitted by the program to verify, not by the environment.
esterel -oc obs3.strl
ocfc2 obs3.oc -B obs3
esterel -oc -causal arbiter4-cyclic.strl
ocfc2 arbiter4-cyclic.oc
fc2symbmin -may Ack_Without_Req_Violated -restrict AckOut1
AckOut2 AckOut3 AckOut4 ocfc2_out.Arbiter4.fc2 obs3.fc2
--- fc2parser: parsing ocfc2_out.Arbiter4.fc2
--- fc2parser: ocfc2_out.Arbiter4.fc2 parsed
--- fc2parser: parsing obs3.AtLeastOneAck4.fc2
--- fc2parser: obs1.AtLeastOneAck4.fc2 parsed
--- fc2symbmin: Results:
--- fc2symbmin: *****************************
--- fc2symbmin: Signal "AT_LEAST_ONE_ACK_VIOLATED" from observer is never emitted
--- fc2symbmin: Output signals from the observer not noticed
are never emitted
Checking liveness properties
duick$ ../../bin/fc2symbmin -must Ack_Always_emitted arbiter4-cyclic.Arbiter4.fc2 obs4.fc2
--- fc2parser: parsing arbiter4-cyclic.Arbiter4.fc2
--- fc2parser: arbiter4-cyclic.Arbiter4.fc2 parsed
--- fc2parser: parsing obs4.fc2
--- fc2parser: obs4.fc2 parsed
signal "Ack_Always_emitted" must be emitted.
Hiding
The esterel encoding ./Lift/lift.strl describes a lift
controller. We want to know if the door is closed when
the lift starts.
We just keep visible the signals OPEN_DOOR,
CLOSE_DOOR, DOOR_CLOSED, LIFT_STARTED, DOOR_OPENED.
We use the following command :
fc2symbmin -see OPEN_DOOR CLOSE_DOOR DOOR_CLOSED
LIFT_STARTED DOOR_OPENED lift.LIFT.fc2 > hiddenLift.fc2.
In reading the fc2 file obtained or looking it with atg,
We can asume the DOOR is tested closed before the lift starts.
Equivalence
If you obtain the fc2 file of ./Arbiter/arbiter.strl from
the two following ways, the automata don't have the same
number of vertice.
esterel -oc -causal arbiter-cyclic.strl
ocfc2 arbiter-cyclic.oc
and
esterel -Lblif -causal arbiter-cyclic.strl
bliffc2 -fc2 arbiter-cyclic.blif
Do these two fc2 files behave equivalent ?
We can check it with the following test equivalence
command:
fc2symbmin -eq ocfc2_out.Arbiter4.fc2 arbiter4-cyclic.fc2 -n
--- fc2parser: parsing ocfc2_out.Arbiter4.fc2
--- fc2parser: ocfc2_out.Arbiter4.fc2 parsed
--- fc2parser: parsing arbiter4-cyclic.fc2
--- fc2parser: arbiter4-cyclic.fc2 parsed
--- fc2symbmin: Global automaton has 11 vertice, 121 transitions
--- fc2min: block 4
--- fc2symbmin: The two automata are equivalent
--- fc2symbmin: Automaton has 4 states, 4 transitions
duick$
If no -n option, the same equivalent automaton is returned.
If the two automata are not equivalent, the -trace option
returns a path going to states not equivalent in fc2 format.
-
-
tutorial.html
Michel Bourdelles
Last modified: Mon Mar 29 12:34:13 MET DST 1999