Loading, Saving, Syntax and Visualization of Automata

Syntax

Automata are encoded in the .dot format. Deterministic automata (DFA, Mealy, Moore) follow the following syntax:

• https://automata.cs.ru.nl/Syntax/Overview

ONFSM follows the Mealy machine syntax, where each possible input/output transition is encoded individually.

digraph g {
  __start0 [label="" shape="none"];
  q0 [shape="circle" margin=0 label="q0"];
  q2 [shape="circle" margin=0 label="q2"];
  q1 [shape="circle" margin=0 label="q1"];
  q0 -> q2 [label="b/1"];
  q0 -> q0 [label="a/0"];
  q0 -> q0 [label="b/2"];
  q0 -> q2 [label="a/1"];
  q2 -> q1 [label="b/0"];
  q2 -> q0 [label="a/2"];
  q1 -> q1 [label="a/2"];
  q1 -> q2 [label="b/0"];
  __start0 -> q1;
}

Markov Decision Processes follow the following syntax:

• each state is encoded as: <state_id> [shape="circle" label=<state_output>];
• each transition is encoded as: <origin_state_id> -> <destination_state_id>[label="<input_action>:<transition_probability>"];

digraph g {
  __start0 [label="" shape="none"];
  28 [shape="circle" label=mud];
  17 [shape="circle" label=grass];
  ...
  28 -> 27 [label="East:1.00"];
  28 -> 26 [label="North:1.00"];
  28 -> 29 [label="South:0.80"];
  28 -> 21 [label="South:0.20"];
  ...
}

Stochastic Transducer(Mealy machine) syntax is similar to the Mealy machine one, just with added transition probability.

• each state is encoded as: <state_id> [shape="circle"];
• each transition is encoded as: <origin_state_id> -> <destination_state_id>[label="<input_action>/:<transition_probability>"];

digraph g {
  __start0 [label="" shape="none"];
  28 <optional label>
  17 <optional label>
  ...
  28 -> 27 [label="East/concrete:1.00"];
  28 -> 26 [label="North/grass:1.00"];
  28 -> 29 [label="South/wall:0.80"];
  28 -> 21 [label="South/grass:0.20"];
  ...
}

For examples, check out following models.

Loading, saving, and visualization of automata

The following code snippet shows how to load automata from the file. When loading automaton form file, specify its automaton_type to one of ['dfa', 'mealy', 'moore', 'mdp', 'smm', 'onfsm'].

For more details, check out the

• https://des-lab.github.io/AALpy/documentation/aalpy/utils/FileHandler.html

from aalpy.utils import save_automaton_to_file, load_automaton_from_file, visualize_automaton

# loading automaton from file
dfa = load_automaton_from_file(path='path_to_the_file', automaton_type='dfa')

# if compute prefixes is set to true, prefix/shortest path to each state will be computed
mealy = load_automaton_from_file(path='path_to_mealy', automaton_type='mealy', compute_prefixes=True)
mdp = load_automaton_from_file(path='path_to_the_file', automaton_type='mdp')

# newer version of aalpy also support
mdp.save()
# write dot representation of the automaton to file
save_automaton_to_file(mdp, path='new_mdp.dot')


# visualize automaton
# supported formats are 'png', 'svg', 'pdf'
dfa.visualize()
# or
visualize_automaton(dfa, file_type='pdf')

# print dot representation of the automaton to standard output
print(dfa)