Module 2.6: CIF tools to view and analyze models

So far, in this module, you have learned to about various properties, such as reachability and deadlock. You have also learned about interaction between automata, through synchronization and the use of shared variables. And you have learned how to compute the state space of models with multiple interacting automata. So far, you have manually computed the state spaces, and manually checked the various properties.

We will now look at some of tools in the CIF toolset that can automate this. We will first look at the CIF explorer, which can automatically compute the state space of CIF models. Then we will look at the CIF to yEd transformer, to visualize CIF models and state spaces. Finally, we will look at the CIF event-based toolset, which has various tools to allow checking properties of CIF state spaces.

The CIF explorer

The CIF explorer can automatically compute the state space of CIF models. To use this tool within the ESCET IDE, right click any CIF model file in the Project Explorer and then select CIF miscellaneous tools and Explore untimed state space.... Since the default settings of the tool typically suffice, click OK to start computing the state space.

The CIF explorer will compute the state space. Progress is shown on the Console tab, and once the computation is completed the number of states and transitions in the state space is printed. For instance, something like the following output could be shown on the console:

                        
                            Found 1 state, 1 state to process.
                            Found 243 states, 0 states to process.
                            Number of states in state space: 243.
                            Number of transitions in state space: 945.
                        
                    

Besides the console output, the CIF explorer will also create a CIF model with a single automaton that represents the state space. And it will write this model to a file.

For instance, consider again the model with two automata, with each two locations, from the previous sub-module. If the first automaton is named aut1 and the second automaton is named aut2, the CIF model could look like this:

                        
                            event a, b, c;

                            automaton aut1:
                                location L1:
                                    initial;
                                    edge b goto L2;

                                location L2:
                                    marked;
                                    edge a goto L1;
                            end

                            automaton aut2:
                                location R1:
                                    initial;
                                    marked;
                                    edge c goto R2;

                                location R2:
                                    edge b goto R1;
                            end
                        
                    

And the CIF model with the generated generated state space could look like this:

                        
                            event a;
                            event b;
                            event c;

                            automaton statespace:
                                alphabet b, a, c;

                                @state(aut1: "L1", aut2: "R1")
                                location loc1:
                                    initial;
                                    edge c goto loc2;

                                @state(aut1: "L1", aut2: "R2")
                                location loc2:
                                    edge b goto loc3;

                                @state(aut1: "L2", aut2: "R1")
                                location loc3:
                                    marked;
                                    edge a goto loc1;
                                    edge c goto loc4;

                                @state(aut1: "L2", aut2: "R2")
                                location loc4:
                                    edge a goto loc2;
                            end
                        
                    

The state space automaton has four locations, and five edges, to represent the four states and 5 transitions of the state space. Each location is annotated with @state, a state annotation. It indicates the state that the location represents. It thus indicates for each automaton its current location, and for each variable its current value. In this case, the CIF model for which the state space is computed has two automata, so for both of them the current location is indicated in each state annotation. For instance, location loc1 represents the state where automaton aut1 is in location L1 and automaton aut2 is in location R1. Location loc3 is marked, which indicates that the corresponding state where automaton aut1 is in location L2 and automaton aut2 is in location R1, is a marked state.

You may have already noticed that the state space automaton has an explicitly declared alphabet. CIF allows to explicitly declare the alphabet of an automaton, but if it is not explicitly specified it is implicitly defined as all the events on the edges of the automaton.

The CIF to yEd transformer

Having the CIF explorer automatically compute a state space is much more efficient then computing it manually. But, looking at the generated state space as a textual CIF model is not as intuitive as the graphical representation of the state space, as we saw in previous sub-modules. Luckily, the CIF toolset includes the CIF to yEd transformer tool. It can be used to transform a CIF models into yEd diagram files. In the ESCET IDE, simply right click any CIF model file in the Project Explorer and then select CIF miscellaneous tools and Convert CIF to yEd diagram.... Click OK to accept the default settings and generate diagrams. You will notice a new file is created whose name ends with .model.graphml, which contains the generated yEd diagram.

The yEd graph editor, or yEd for short, can then be used view such generated diagrams. yEd is freely available and runs on Windows, Linux and macOS. You can download it at yEd website. After you have installed the tool, and assuming you let the .graphml file extension be coupled to yEd, simply double clicking on a .model.graphml file in the ESCET IDE is enough to open it in yEd. By default, the model will not have any layout, so all elements of the CIF model appear on top of each other:

yEd can automatically layout graphs. Click the Layout menu and select One-Click Layout to let yEd automatically layout the diagram. Alternatively, select the One-Click Layout button on the toolbar. The diagram then could look something like this:

As you can see, yEd typically does quite a good job at layouting. In the diagram it is much easier to see the transitions between the various states of the state space, then it is in the textual CIF model.

The CIF to yEd transformer can not just generate diagrams for a state space, but for any CIF model. As an example, consider the diagram for the production line from earlier in this module:

Besides a 'model' diagram, a graphical representation of the CIF model, the CIF to yEd transformer also generates a 'relations' diagram. These diagrams are generated in files whose names end with .relations.graphml. Such diagram are especially useful for models with multiple interacting automata. For instance, for the production system, the generated relations diagram could look like this:

Various elements of the CIF model are shown as shapes labeled with their names, including the automata, locations and variables. Furthermore, for each use of an event a circle is drawn and linked with an edge to the declaration of the event. This allows to more quickly and visually see which automata synchronize over an event. For each variable, arrows are drawn from the variable declaration to the elements of the model where the variable is used, such as the locations that have outgoing edges that use the variable in their guards or updates.

The CIF event-based toolset

The CIF event-based toolset is a collection of tools that can among others be used to analyze and manipulate CIF models. These tools only work on 'simple' CIF models, and for instance do not support models with variables. If you have a model with variables, you can use the CIF explorer to first compute the state space model, and use that state space model with the event-based tools.

For instance, a model can be checked for being trim. This relates to properties we learned about earlier in this module. A model is trim if for every automaton, every location is reachable from an initial location, and every location is also co-reachable, that is, it is possible to reach a marked location from it. The term co-reachable is just another term for being non-blocking. To run the check, right click a CIF model in the Project Explorer and choose CIF synthesis tools, Event-based synthesis tools and Apply trim check.... Confirm the default settings by clicking OK. A file is created whose name ends with _trimcheck.txt. Open it to inspect the result of the check. Consider for instance the following example result:

                        
                            Trim check FAILS in file "example.cif".

                            Trim check FAILS for automaton "aut1".
                            - All locations are reachable.
                            - The following location is not coreachable:
                              location "aut1.l2".
                        
                    

It indicates that the model failed the check and is thus not trim. All locations of automaton aut1 are reachable, but its location l2 is not co-reachable. Location l2 is thus blocking. If the model being checked is not trim, and error message is also shown on the Console tab.

Previously in this module, we discussed non-deterministic automata. These are not supported by most of the tools in the event-based toolset. To transform a model with a non-deterministic automaton to a deterministic one, you can use the NFA to DFA automaton conversion. To execute the conversion, right click a CIF model in the Project Explorer and choose CIF synthesis tools, Event-based synthesis tools and Apply NFA to DFA automaton conversion.... Confirm the default settings by clicking OK. A file is created whose name ends with _dfa.cif. Open it to inspect the result of the conversion.

The event-based toolset contains various other tools. For instance, it has a tool to check whether the languages of two models are the same, and a tool to convert a non-trim model into a trim one.

Quiz

                                        
                                            event e, f, g, h;

                                            automaton a:
                                                location:
                                                    initial;
                                                    marked;
                                                    edge e, f, g;
                                            end

                                            automaton b:
                                                alphabet f, g, h;

                                                location:
                                                    initial;
                                                    marked;
                                                    edge g, h;
                                            end