xref: /linux/tools/verification/dot2/automata.py (revision 7f71507851fc7764b36a3221839607d3a45c2025)
1#!/usr/bin/env python3
2# SPDX-License-Identifier: GPL-2.0-only
3#
4# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
5#
6# Automata object: parse an automata in dot file digraph format into a python object
7#
8# For further information, see:
9#   Documentation/trace/rv/deterministic_automata.rst
10
11import ntpath
12
13class Automata:
14    """Automata class: Reads a dot file and part it as an automata.
15
16    Attributes:
17        dot_file: A dot file with an state_automaton definition.
18    """
19
20    invalid_state_str = "INVALID_STATE"
21
22    def __init__(self, file_path):
23        self.__dot_path = file_path
24        self.name = self.__get_model_name()
25        self.__dot_lines = self.__open_dot()
26        self.states, self.initial_state, self.final_states = self.__get_state_variables()
27        self.events = self.__get_event_variables()
28        self.function = self.__create_matrix()
29
30    def __get_model_name(self):
31        basename = ntpath.basename(self.__dot_path)
32        if not basename.endswith(".dot") and not basename.endswith(".gv"):
33            print("not a dot file")
34            raise Exception("not a dot file: %s" % self.__dot_path)
35
36        model_name = ntpath.splitext(basename)[0]
37        if model_name.__len__() == 0:
38            raise Exception("not a dot file: %s" % self.__dot_path)
39
40        return model_name
41
42    def __open_dot(self):
43        cursor = 0
44        dot_lines = []
45        try:
46            dot_file = open(self.__dot_path)
47        except:
48            raise Exception("Cannot open the file: %s" % self.__dot_path)
49
50        dot_lines = dot_file.read().splitlines()
51        dot_file.close()
52
53        # checking the first line:
54        line = dot_lines[cursor].split()
55
56        if (line[0] != "digraph") and (line[1] != "state_automaton"):
57            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
58        else:
59            cursor += 1
60        return dot_lines
61
62    def __get_cursor_begin_states(self):
63        cursor = 0
64        while self.__dot_lines[cursor].split()[0] != "{node":
65            cursor += 1
66        return cursor
67
68    def __get_cursor_begin_events(self):
69        cursor = 0
70        while self.__dot_lines[cursor].split()[0] != "{node":
71            cursor += 1
72        while self.__dot_lines[cursor].split()[0] == "{node":
73            cursor += 1
74        # skip initial state transition
75        cursor += 1
76        return cursor
77
78    def __get_state_variables(self):
79        # wait for node declaration
80        states = []
81        final_states = []
82
83        has_final_states = False
84        cursor = self.__get_cursor_begin_states()
85
86        # process nodes
87        while self.__dot_lines[cursor].split()[0] == "{node":
88            line = self.__dot_lines[cursor].split()
89            raw_state = line[-1]
90
91            #  "enabled_fired"}; -> enabled_fired
92            state = raw_state.replace('"', '').replace('};', '').replace(',','_')
93            if state[0:7] == "__init_":
94                initial_state = state[7:]
95            else:
96                states.append(state)
97                if "doublecircle" in self.__dot_lines[cursor]:
98                    final_states.append(state)
99                    has_final_states = True
100
101                if "ellipse" in self.__dot_lines[cursor]:
102                    final_states.append(state)
103                    has_final_states = True
104
105            cursor += 1
106
107        states = sorted(set(states))
108        states.remove(initial_state)
109
110        # Insert the initial state at the bein og the states
111        states.insert(0, initial_state)
112
113        if not has_final_states:
114            final_states.append(initial_state)
115
116        return states, initial_state, final_states
117
118    def __get_event_variables(self):
119        # here we are at the begin of transitions, take a note, we will return later.
120        cursor = self.__get_cursor_begin_events()
121
122        events = []
123        while self.__dot_lines[cursor].lstrip()[0] == '"':
124            # transitions have the format:
125            # "all_fired" -> "both_fired" [ label = "disable_irq" ];
126            #  ------------ event is here ------------^^^^^
127            if self.__dot_lines[cursor].split()[1] == "->":
128                line = self.__dot_lines[cursor].split()
129                event = line[-2].replace('"','')
130
131                # when a transition has more than one lables, they are like this
132                # "local_irq_enable\nhw_local_irq_enable_n"
133                # so split them.
134
135                event = event.replace("\\n", " ")
136                for i in event.split():
137                    events.append(i)
138            cursor += 1
139
140        return sorted(set(events))
141
142    def __create_matrix(self):
143        # transform the array into a dictionary
144        events = self.events
145        states = self.states
146        events_dict = {}
147        states_dict = {}
148        nr_event = 0
149        for event in events:
150            events_dict[event] = nr_event
151            nr_event += 1
152
153        nr_state = 0
154        for state in states:
155            states_dict[state] = nr_state
156            nr_state += 1
157
158        # declare the matrix....
159        matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
160
161        # and we are back! Let's fill the matrix
162        cursor = self.__get_cursor_begin_events()
163
164        while self.__dot_lines[cursor].lstrip()[0] == '"':
165            if self.__dot_lines[cursor].split()[1] == "->":
166                line = self.__dot_lines[cursor].split()
167                origin_state = line[0].replace('"','').replace(',','_')
168                dest_state = line[2].replace('"','').replace(',','_')
169                possible_events = line[-2].replace('"','').replace("\\n", " ")
170                for event in possible_events.split():
171                    matrix[states_dict[origin_state]][events_dict[event]] = dest_state
172            cursor += 1
173
174        return matrix
175