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