print · login   

Check equivalence of models

Checking equivalence is useful for verifying the learning tool by checking equivalence of a learned model with a known teacher model. Currently we support equivalence checking of a subset of EFSM models supported by the Sut tool.

Important: for equivalence checking the Sut tool also needs the CADP tool set installed.

To compare two models we then can just use the sut_compare command which internally uses the CADP tool set.

Thus we can do equivalence checking as follows: 

    > sut_compare model1.xml model2.xml 0 2
    ...
    TRUE or FALSE with a trace

The equivalence prints TRUE in case of equivalence, otherwise it prints FALSE followed by the trace showing the difference between the models.

The parameters 0 and 2 specify the range used for bisimulation checking. This range is needed when the learned Extended Finite State Machine (EFSM)
is transformed into a LOTOS specification by means of the CADPtool set. We have to limit the range of data parameters in order to check the equivalence in a limited amount of time.

Notes:

  • sut_compare can compare register automata(with data), mealy automata(no data), and lts automata.
  • Also different equivalences can be checked with the CADP toolset. The CADP equivalence type 'strong' is used by default. For more types see the documentation for the bisimulator.
  • Internally sut_compare does the following:
    • if an input model is a REGISTER automata it converts it using the command 'sut_uppaal2lotos' to a lotos model where a data range is applied in the lotos model. Using the svl command of the CADP toolset this model is flattened to a bcg model which is just an LTS stored in a binary format.
    • if an input model is a MEALY automata without data specified in a LTS file format, where label="input/output", then it converts it to the aut format in which the input and transitions are split. The aut model again is converted, using the bcg_io command of the CADP toolset, to a bcg model.
    • if an input model is a LTS automata, you must specify the --lts flag, and then it converts it to the aut format which again is converted, using the bcg_io command of the CADP toolset, to a bcg model.
    • by default io mealy machine comparison is done ( --iomealy flag ) instead of lts comparison ( --lts flag ). The difference is that for mealy automata two automata can differ in output for some input. However for lts automata two automata differ in the sense that one automata has a transition for label X and the other doesn't.
    • when both models are converted to the bcg format then those bcg models are compared using the bcg_open command bisimulator from the CADP toolset :

            bcg_open model1.bcg bisimulator -diag -bfs -strong model2.bcg