xref: /linux/tools/verification/dot2/automata.py (revision 40648d246fa4307ef11d185933cb0d79fc9ff46c)
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, model_name=None):
23        self.__dot_path = file_path
24        self.name = model_name or 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        self.events_start, self.events_start_run = self.__store_init_events()
30
31    def __get_model_name(self):
32        basename = ntpath.basename(self.__dot_path)
33        if not basename.endswith(".dot") and not basename.endswith(".gv"):
34            print("not a dot file")
35            raise Exception("not a dot file: %s" % self.__dot_path)
36
37        model_name = ntpath.splitext(basename)[0]
38        if model_name.__len__() == 0:
39            raise Exception("not a dot file: %s" % self.__dot_path)
40
41        return model_name
42
43    def __open_dot(self):
44        cursor = 0
45        dot_lines = []
46        try:
47            dot_file = open(self.__dot_path)
48        except:
49            raise Exception("Cannot open the file: %s" % self.__dot_path)
50
51        dot_lines = dot_file.read().splitlines()
52        dot_file.close()
53
54        # checking the first line:
55        line = dot_lines[cursor].split()
56
57        if (line[0] != "digraph") and (line[1] != "state_automaton"):
58            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
59        else:
60            cursor += 1
61        return dot_lines
62
63    def __get_cursor_begin_states(self):
64        cursor = 0
65        while self.__dot_lines[cursor].split()[0] != "{node":
66            cursor += 1
67        return cursor
68
69    def __get_cursor_begin_events(self):
70        cursor = 0
71        while self.__dot_lines[cursor].split()[0] != "{node":
72            cursor += 1
73        while self.__dot_lines[cursor].split()[0] == "{node":
74            cursor += 1
75        # skip initial state transition
76        cursor += 1
77        return cursor
78
79    def __get_state_variables(self):
80        # wait for node declaration
81        states = []
82        final_states = []
83
84        has_final_states = False
85        cursor = self.__get_cursor_begin_states()
86
87        # process nodes
88        while self.__dot_lines[cursor].split()[0] == "{node":
89            line = self.__dot_lines[cursor].split()
90            raw_state = line[-1]
91
92            #  "enabled_fired"}; -> enabled_fired
93            state = raw_state.replace('"', '').replace('};', '').replace(',','_')
94            if state[0:7] == "__init_":
95                initial_state = state[7:]
96            else:
97                states.append(state)
98                if "doublecircle" in self.__dot_lines[cursor]:
99                    final_states.append(state)
100                    has_final_states = True
101
102                if "ellipse" in self.__dot_lines[cursor]:
103                    final_states.append(state)
104                    has_final_states = True
105
106            cursor += 1
107
108        states = sorted(set(states))
109        states.remove(initial_state)
110
111        # Insert the initial state at the bein og the states
112        states.insert(0, initial_state)
113
114        if not has_final_states:
115            final_states.append(initial_state)
116
117        return states, initial_state, final_states
118
119    def __get_event_variables(self):
120        # here we are at the begin of transitions, take a note, we will return later.
121        cursor = self.__get_cursor_begin_events()
122
123        events = []
124        while self.__dot_lines[cursor].lstrip()[0] == '"':
125            # transitions have the format:
126            # "all_fired" -> "both_fired" [ label = "disable_irq" ];
127            #  ------------ event is here ------------^^^^^
128            if self.__dot_lines[cursor].split()[1] == "->":
129                line = self.__dot_lines[cursor].split()
130                event = line[-2].replace('"','')
131
132                # when a transition has more than one lables, they are like this
133                # "local_irq_enable\nhw_local_irq_enable_n"
134                # so split them.
135
136                event = event.replace("\\n", " ")
137                for i in event.split():
138                    events.append(i)
139            cursor += 1
140
141        return sorted(set(events))
142
143    def __create_matrix(self):
144        # transform the array into a dictionary
145        events = self.events
146        states = self.states
147        events_dict = {}
148        states_dict = {}
149        nr_event = 0
150        for event in events:
151            events_dict[event] = nr_event
152            nr_event += 1
153
154        nr_state = 0
155        for state in states:
156            states_dict[state] = nr_state
157            nr_state += 1
158
159        # declare the matrix....
160        matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
161
162        # and we are back! Let's fill the matrix
163        cursor = self.__get_cursor_begin_events()
164
165        while self.__dot_lines[cursor].lstrip()[0] == '"':
166            if self.__dot_lines[cursor].split()[1] == "->":
167                line = self.__dot_lines[cursor].split()
168                origin_state = line[0].replace('"','').replace(',','_')
169                dest_state = line[2].replace('"','').replace(',','_')
170                possible_events = line[-2].replace('"','').replace("\\n", " ")
171                for event in possible_events.split():
172                    matrix[states_dict[origin_state]][events_dict[event]] = dest_state
173            cursor += 1
174
175        return matrix
176
177    def __store_init_events(self):
178        events_start = [False] * len(self.events)
179        events_start_run = [False] * len(self.events)
180        for i, _ in enumerate(self.events):
181            curr_event_will_init = 0
182            curr_event_from_init = False
183            curr_event_used = 0
184            for j, _ in enumerate(self.states):
185                if self.function[j][i] != self.invalid_state_str:
186                    curr_event_used += 1
187                if self.function[j][i] == self.initial_state:
188                    curr_event_will_init += 1
189            if self.function[0][i] != self.invalid_state_str:
190                curr_event_from_init = True
191            # this event always leads to init
192            if curr_event_will_init and curr_event_used == curr_event_will_init:
193                events_start[i] = True
194            # this event is only called from init
195            if curr_event_from_init and curr_event_used == 1:
196                events_start_run[i] = True
197        return events_start, events_start_run
198
199    def is_start_event(self, event):
200        return self.events_start[self.events.index(event)]
201
202    def is_start_run_event(self, event):
203        # prefer handle_start_event if there
204        if any(self.events_start):
205            return False
206        return self.events_start_run[self.events.index(event)]
207