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