Skip to content

Transition System

TranSys

Transition system class. T = (S, A, delta, S_init, AP, L).

Parameters:

Name Type Description Default
transition_system_input

input format for states,

 None
S

states

 None
A

actions

 None
E

transition relation

 None
I

initial_states

 None
AP_dict

the set of atomic propositions

 None
L

labels

 None
Source code in src/floras/components/transition_system.py 
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
class TranSys():
    """Transition system class.
    T = (S, A, delta, S_init, AP, L).

    Args:
        transition_system_input: input format for states,
        transitions, initial states, and labels.
        S: states
        A: actions
        E: transition relation
        I: initial_states
        AP_dict: the set of atomic propositions
        L: labels
    """
    def __init__(
            self, transition_system_input=None, S=None,
            A=None, E=None, I=None, AP_dict=None, L=None  # noqa: E741
            ):
        self.S = S
        self.A = A
        self.E = E
        self.I = I  # noqa: E741
        self.AP_dict = AP_dict
        self.Sigma = None
        self.AP = None
        self.L = None
        self.G = None
        self.custom_map = None
        self.input = transition_system_input
        if self.input:
            self.setup()
            self.custom_map = transition_system_input.custom_map

    def setup(self):
        """
        Set up the transition system from the input data.
        """
        self.S = list(self.input.states)
        self.A = ['act' + str(k) for k in range(0, 8)]
        self.construct_transition_function()
        self.get_APs()
        self.construct_initial_conditions()
        self.construct_labels()

    def print_transitions(self):
        """
        Print all transitions.
        """
        for e_out, e_in in self.E.items():
            print("node out: " + str(e_out) + " node in: " + str(e_in))

    def construct_transition_function(self):
        """
        Create the set of edges E from the input data.
        """
        self.E = dict()
        for s in self.input.states:
            i = 0
            for ns in self.input.transitions[s]:
                self.E[(s, 'act' + str(i))] = ns
                i += 1

    def get_APs(self):
        """
        Set of atomic propositions required to define a specification.
        Need not initialize all cells of the grid as APs, only
        the relevant states to define what the agent must do.
        Need to setup atomic propositions.
        """
        self.AP_dict = od()
        for s in self.S:  # If the system state is the init or goal
            self.AP_dict[s] = []
            if s in self.input.labels:
                labels = self.input.labels[s]
                for label in labels:
                    self.AP_dict[s].append(spot.formula.ap(label))

    def construct_initial_conditions(self):
        """
        Set the initial state.
        """
        self.I = self.input.init  # noqa: E741

    def construct_labels(self):
        """
        Add the labels to the states in the form of spot formulas.
        """
        self.L = od()
        for s in self.S:
            if s in self.AP_dict.keys():
                self.L[s] = set(self.AP_dict[s])
            else:
                self.L[s] = {}

    def save_plot(self, fn):
        """
        Save a pdf of the graph of the transition system.

        Args:
            fn: Filename to store the figure under `filename.pdf'.
        """
        self.G = nx.DiGraph()
        self.G.add_nodes_from(list(self.S))

        edges = []
        edge_attr = dict()
        # node_attr = dict()
        for state_act, in_node in self.E.items():
            out_node = state_act[0]
            act = state_act[1]
            edge = (out_node, in_node)
            edge_attr[edge] = {"act": act}
            edges.append(edge)
        self.G.add_edges_from(edges)
        nx.set_edge_attributes(self.G, edge_attr)

        G_agr = nx.nx_agraph.to_agraph(self.G)
        G_agr.node_attr['style'] = 'filled'
        G_agr.node_attr['gradientangle'] = 90

        for i in G_agr.nodes():
            n = G_agr.get_node(i)
            n.attr['fillcolor'] = 'white'
            n.attr['shape'] = 'circle'

        if not os.path.exists("imgs"):
            os.makedirs("imgs")
        G_agr.draw("imgs/" + fn + ".pdf", prog='dot')

construct_initial_conditions()

Set the initial state.

Source code in src/floras/components/transition_system.py 
106
107
108
109
110
def construct_initial_conditions(self):
    """
    Set the initial state.
    """
    self.I = self.input.init  # noqa: E741

construct_labels()

Add the labels to the states in the form of spot formulas.

Source code in src/floras/components/transition_system.py 
112
113
114
115
116
117
118
119
120
121
def construct_labels(self):
    """
    Add the labels to the states in the form of spot formulas.
    """
    self.L = od()
    for s in self.S:
        if s in self.AP_dict.keys():
            self.L[s] = set(self.AP_dict[s])
        else:
            self.L[s] = {}

construct_transition_function()

Create the set of edges E from the input data.

Source code in src/floras/components/transition_system.py 
80
81
82
83
84
85
86
87
88
89
def construct_transition_function(self):
    """
    Create the set of edges E from the input data.
    """
    self.E = dict()
    for s in self.input.states:
        i = 0
        for ns in self.input.transitions[s]:
            self.E[(s, 'act' + str(i))] = ns
            i += 1

get_APs()

Set of atomic propositions required to define a specification. Need not initialize all cells of the grid as APs, only the relevant states to define what the agent must do. Need to setup atomic propositions.

Source code in src/floras/components/transition_system.py 
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
def get_APs(self):
    """
    Set of atomic propositions required to define a specification.
    Need not initialize all cells of the grid as APs, only
    the relevant states to define what the agent must do.
    Need to setup atomic propositions.
    """
    self.AP_dict = od()
    for s in self.S:  # If the system state is the init or goal
        self.AP_dict[s] = []
        if s in self.input.labels:
            labels = self.input.labels[s]
            for label in labels:
                self.AP_dict[s].append(spot.formula.ap(label))

print_transitions()

Print all transitions.

Source code in src/floras/components/transition_system.py 
73
74
75
76
77
78
def print_transitions(self):
    """
    Print all transitions.
    """
    for e_out, e_in in self.E.items():
        print("node out: " + str(e_out) + " node in: " + str(e_in))

save_plot(fn)

Save a pdf of the graph of the transition system.

Parameters:

Name Type Description Default
fn

Filename to store the figure under `filename.pdf'.

 required
Source code in src/floras/components/transition_system.py 
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
def save_plot(self, fn):
    """
    Save a pdf of the graph of the transition system.

    Args:
        fn: Filename to store the figure under `filename.pdf'.
    """
    self.G = nx.DiGraph()
    self.G.add_nodes_from(list(self.S))

    edges = []
    edge_attr = dict()
    # node_attr = dict()
    for state_act, in_node in self.E.items():
        out_node = state_act[0]
        act = state_act[1]
        edge = (out_node, in_node)
        edge_attr[edge] = {"act": act}
        edges.append(edge)
    self.G.add_edges_from(edges)
    nx.set_edge_attributes(self.G, edge_attr)

    G_agr = nx.nx_agraph.to_agraph(self.G)
    G_agr.node_attr['style'] = 'filled'
    G_agr.node_attr['gradientangle'] = 90

    for i in G_agr.nodes():
        n = G_agr.get_node(i)
        n.attr['fillcolor'] = 'white'
        n.attr['shape'] = 'circle'

    if not os.path.exists("imgs"):
        os.makedirs("imgs")
    G_agr.draw("imgs/" + fn + ".pdf", prog='dot')

setup()

Set up the transition system from the input data.

Source code in src/floras/components/transition_system.py 
62
63
64
65
66
67
68
69
70
71
def setup(self):
    """
    Set up the transition system from the input data.
    """
    self.S = list(self.input.states)
    self.A = ['act' + str(k) for k in range(0, 8)]
    self.construct_transition_function()
    self.get_APs()
    self.construct_initial_conditions()
    self.construct_labels()

TransitionSystemInput

Input format containing data to create a transition system.

Parameters:

Name Type Description Default
states

States of the system model.

 required
transitions

Transitions between system states.

 required
labels

Labels of each system state.

 required
init

Initial state of the system.

 required
Source code in src/floras/components/transition_system.py 
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
class TransitionSystemInput():
    """Input format containing data to create a transition system.

    Args:
        states: States of the system model.
        transitions: Transitions between system states.
        labels: Labels of each system state.
        init: Initial state of the system.
    """
    def __init__(self, states, transitions, labels, init, custom_map=None):
        self.states = states
        self.transitions = transitions
        self.labels = labels
        self.init = init
        self.next_state_dict = None
        self.custom_map = custom_map
        self.setup()

    def setup(self):
        self.next_state_dict = self.transitions