Tomás Barros
In order to work with our parameterized formalism, we have developed a tool, named FC2Instantiate, to get instantiations from the parameterized descriptions given the finite abstract domain of their unbounded parameters. Both description and domains inputs are in FC2Parameterized format, the output of the tool is standard FC2 format.
In this section we describe the syntax of the FC2Parameterized format and the use of the tool FC2Instantiate through a guided example.
Given a system of communicating automata with parameters and the domain of its unbounded parameters, FC2Instantiate is a tool, 100% written in Java, that generates a finite system of communicating automata by translating each of the parameters to all the values in its domain.
We start by reviewing the FC2 format, necessary to a better understanding of its extension, FC2Parameterized.