How-To use ramona

You can find a list of possible options for the tool using option -h. By default ramona uses option -W, that computes the (weak) state class graph for the system given as input. You can also use option -G that is an experimental construction that should produce more compact graphs. We are actively working on improving this construction.

$ ramona -h
Usage of ramona.exe:
  -G    compact SSCG (experimental)
  -W    state class graph preserving states and LTL (SSCG)
  -pdf  string
        name of file for pdf output
  -q    textual output (digest)
  -svg  string
        name of file for svg output
  -v    textual output (full)

Option -q gives you some statistics on the size of the generated graph while option -v gives you a full textual output of the graph, complete with information on timing constraints.

$ ramona -q t1.task
# 3 Tasks
# id  period  duration  offset
#  0      10         3   [1,1]
#  1      15         2   [0,0]
#  2      15         2   [0,0]
# states 30
# transitions 37

For small systems (with state graphs that have less than 500 classes), you can output a graphical representation generated from GraphViz. You need to install GraphViz in your machine for this to work; see for example the SVG file generated from the command:

$ ramona -svg t1.svg t1.task