Related Tool
TRE2TA
By tre2ta, you can translate a timed regular expression to a timed automaton. You can visualize the generated timed regular expression by visualize-monaa-dot
for example.
Installation by Homebrew (for macOS)
- Set up homebrew (See the official web page)
- Install tre2ta (and also monaa) by
brew install maswag/scientific/monaa
Docker
- Install docker
- pull the docker image by
docker pull maswag/tre2ta
. - Use the container e.g.,
docker run -i maswag/tre2ta -e '(AB)$'
.
Installation from source
1. Build tre2ta
cd /path/to/monaa
mkdir -p build
cd build && cmake -DCMAKE_BUILD_TYPE=Release .. && make tre2ta
2. (Optional) Install the executable and the manual
sudo install -m755 tre2ta /usr/local/bin
sudo install -m644 ../doc/tre2ta.1 /usr/local/share/man/man1/
visualize-monaa-dot
Visualize-monaa-dot is a tool to translate a DOT file for MONAA to the DOT file suitable for visualization by Graphviz. For example, the following DOT language is visualized as the following graph through Graphviz.
digraph G {
1 [init=1,match=0];
2 [init=0,match=0];
3 [init=0,match=1];
1->2 [label=A,reset="{0}",guard="{x0 < 1}"];
2->1 [label=B,reset="{0}",guard="{x0 < 1}"];
2->1 [label=C,reset="{0}",guard="{x0 < 1}"];
2->3 [label="$",guard="{x0 > 1}"];
}
Visualize-monaa-dot reads DOT for MONAA from the standard input and it outputs DOT for Graphviz to the standard output. Therefore, for example, the whole process to create an svg file (example.svg
) from a DOT file (example.dot
) is as follows.
visualize-monaa-dot-exe < example.dot | dot -T svg -o example.svg
Since visualize-monaa-dot uses the graphviz package of Haskell for DOT language parsing, while MONAA uses the Boost Graph Library, their supported DOT languages have slight difference.
monaa2imitator
monaa2imitator is a tool to translate a DOT file for MONAA to the modeling language of IMITATOR. For example, the following timed automaton in DOT is translated to the following.
digraph G {
loc1 [init=1,match=0];
loc2 [init=0,match=0];
loc3 [init=0,match=1];
loc1->loc2 [label=A,reset="{0}",guard="{x0 < 1}"];
loc2->loc1 [label=B,reset="{0}",guard="{x0 < 1}"];
loc2->loc1 [label=C,reset="{0}",guard="{x0 < 1}"];
loc2->loc3 [label=D,guard="{x0 > 1}"];
}
var
x0,
: clock;
(************************************************************)
automaton G
(************************************************************)
synclabs: A, B, C, D;
loc dummyInitLoc: invariant True
when True do {x0 := 0} goto loc1;
loc loc1: invariant True
when x0 < 1 sync A do {x0 := 0} goto loc2;
loc loc2: invariant True
when x0 < 1 sync B do {x0 := 0} goto loc1;
when x0 < 1 sync C do {x0 := 0} goto loc1;
when x0 > 1 sync D goto loc3;
loc loc3: invariant True
end (* G *)
(************************************************************)
(* Initial state *)
(************************************************************)
init :=
(*------------------------------------------------------------*)
(* Initial location *)
(*------------------------------------------------------------*)
& loc[G] = dummyInitLoc
(*------------------------------------------------------------*)
(* Initial clock constraints *)
(*------------------------------------------------------------*)
& x0 = 0
(*------------------------------------------------------------*)
(* Parameter constraints *)
(*------------------------------------------------------------*)
;
(************************************************************)
(* The end *)
(************************************************************)
end
The usage of monaa2imitator
is as follows.
# Via docker
docker run -i maswag/monaa2imitator < example.dot > example.imi
# Naitive build with stack
stack run < ./example.dot > example.imi