Flatten EFSM model with data to FSM model

Flattening is useful for learning a SUT with data parameters for a limited range of its parameters. Note: with flattening we mean removing data parameters from input actions by defining for each input instead a set of symbols where each symbol presents an unique instance of its input parameters from the given range.

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

Flattening at work

To flatten a Sut model in a uppaal file to mealy fsm in dot format

• if you flatten an uppaal model using cadp via the lotos path to a .bcg file

      sut_uppaal2bcg model.uppaal.xml model.bcg 0 2

Here [0:2] is the range we take for the data parameters in the inputs. You are free to choose any continous range. The format .bcg is binary coded graphs. Note: both input as output model have input and output on a separate transition.

• the .bcg file can be converted to an .aut file which always has state 0 as start state with

      bcg_io model.bcg model.aut

The format .aut is aldebaran format. Note: both input as output model have input and output on a separate transition.

• then you can convert this to a mealy machine in a dot file

      sut_ioaut2mealydot model.aut model.dot

The format .dot is graph description language. In the output model the input and output of a mealy machine's transition are now combined in a single transition. This last step can be only done for fsm io-automata which have alternating input and output.

The final result file model.dot contains the flat mealy model!