4 Transition Systems
Besides graph representation and traversal, JAGAL also considers transition systems. Transition systems are used in the computation and automata theory and describe possible states in a state-based system. Relations between the states are called transitions.
A transition system has a non-empty set of start states and a set of final states.
Transition systems can be represented by directed graphs, where the vertices are states connected by transitions. The edges can either have labels or not.
In the following sections we will show the different types of transition systems as well as JAGAL’s serialization and parsing functionalities.
4.1 Unlabelled Transition Systems
A good example for transition system without transition labels is a finite-state machine representing a traffic light. It has the states S = {r, ry, g, y}, where r, y, and g stand for the colors red, yellow, and green. While operating the traffic lights change the states in the following order, where all of the states can be start states:
r → ry → g → y → r
In the JAGAL framework, this transition system can be built in the following way:
TransitionSystem ts = new TransitionSystem();
ts.addState("r");
ts.addState("ry");
ts.addState("y");
ts.addState("g");
ts.addStartState("r");
ts.addRelation("r", "ry");
ts.addRelation("ry", "g");
ts.addRelation("g", "y");
ts.addRelation("y", "r");
Since the class TransitionSystem inherits from AbstractGraph and thus implements the Traversable interface, we can traverse through a transition system and also use all the methods we can use on graphs.
4.2 Labelled Transition Systems
Transition systems can be complemented by transition labels. In the graph representation, transition labels are edge labels. Labels can represent different things depending on the user’s interest. Often, they are seen as conditions that must hold true or events that must be triggered to reach the next state.
As an example we want to build a deterministic finite automata (DFA) with the alphabet Σ = {0, 1}, that only accepts words containing the symbol sequence 01. The corresponding transition system looks like the following:
The transition system can also be represented in JAGAL:
LabeledTransitionSystem l = new LabeledTransitionSystem();
l.addState("a");
l.addState("b");
l.addState("c");
l.addState("d");
l.addStartState("a");
l.addEndState("d");
l.addEvent("0");
l.addEvent("1");
l.addRelation("a", "b", "1");
l.addRelation("a", "c", "0");
l.addRelation("b", "b", "1");
l.addRelation("b", "c", "0");
l.addRelation("c", "c", "0");
l.addRelation("c", "d", "1");
l.addRelation("d", "d", "0");
l.addRelation("d", "d", "1");
Since we defined exactly one start state and the transition system is deterministic, the finite-state machine is a DFA. This property can also be checked by using the isDFA() method. With the method acceptsSequence(String… s) we can check if an input sequence gets accepted by the DFA or not:
System.out.println(l.acceptsSequence("0", "0", "1", "0"));
// true
System.out.println(l.acceptsSequence("1", "1", "0", "0"));
// false
Once again we can use the visualization classes to generate a graphical output of the transition system (see figure 2):
new DisplayFrame(new LabeledTransitionSystemComponent(l), true);
Figure 2: Visualization of an instance of the LabeledTransitionSystem class.
4.3 Serializing Transition Systems
To store transition systems and make them available for other users and tools, the JAGAL framework comes with a serialization functionality. Although the serializing classes are prepared for supporting different output formats, currently only the Petrify file format is supported. The serializer takes a transition system, the target format and the path as argument and serializes the transition system.
TSSerialization.serialize(l, TSSerializationFormat.PETRIFY,
"test-ts", "/arbitrary/path");
The labelled transition system gets stored under the file name test-ts.sg. Since l refers to the transition system from the last subsection, the generated file contains the following information (a # indicates the beginning of a comment):
.outputs 1 0 # Labels .state graph
a1b # Transitions a0c
b1b
b0c
c0c
c1d
d0d
d1d
.marking {a} # Start marking
.final {d} # Final states
.end
Transition systems in the Petrify file format can also be parsed using JAGAL’s built in parser. It recognizes the file type by the file extension and returns an instance of AbstractLabeledTransitionSystem.
AbstractLabeledTransitionSystem lts = TSParser.parse(
new File("/arbitrary/path/test-ts.sg"));
The resulting transition system can be used just like any other transition system object we defined by hand.