verification/dot2/automata.py

0001 #!/usr/bin/env python3
0002 # SPDX-License-Identifier: GPL-2.0-only
0003 #
0004 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
0005 #
0006 # Automata object: parse an automata in dot file digraph format into a python object
0007 #
0008 # For further information, see:
0009 #   Documentation/trace/rv/deterministic_automata.rst
0010
0011 import ntpath
0012
0013 class Automata:
0014     """Automata class: Reads a dot file and part it as an automata.
0015
0016     Attributes:
0017         dot_file: A dot file with an state_automaton definition.
0018     """
0019
0020     invalid_state_str = "INVALID_STATE"
0021
0022     def __init__(self, file_path):
0023         self.__dot_path = file_path
0024         self.name = self.__get_model_name()
0025         self.__dot_lines = self.__open_dot()
0026         self.states, self.initial_state, self.final_states = self.__get_state_variables()
0027         self.events = self.__get_event_variables()
0028         self.function = self.__create_matrix()
0029
0030     def __get_model_name(self):
0031         basename = ntpath.basename(self.__dot_path)
0032         if basename.endswith(".dot") == False:
0033             print("not a dot file")
0034             raise Exception("not a dot file: %s" % self.__dot_path)
0035
0036         model_name = basename[0:-4]
0037         if model_name.__len__() == 0:
0038             raise Exception("not a dot file: %s" % self.__dot_path)
0039
0040         return model_name
0041
0042     def __open_dot(self):
0043         cursor = 0
0044         dot_lines = []
0045         try:
0046             dot_file = open(self.__dot_path)
0047         except:
0048             raise Exception("Cannot open the file: %s" % self.__dot_path)
0049
0050         dot_lines = dot_file.read().splitlines()
0051         dot_file.close()
0052
0053         # checking the first line:
0054         line = dot_lines[cursor].split()
0055
0056         if (line[0] != "digraph") and (line[1] != "state_automaton"):
0057             raise Exception("Not a valid .dot format: %s" % self.__dot_path)
0058         else:
0059             cursor += 1
0060         return dot_lines
0061
0062     def __get_cursor_begin_states(self):
0063         cursor = 0
0064         while self.__dot_lines[cursor].split()[0] != "{node":
0065             cursor += 1
0066         return cursor
0067
0068     def __get_cursor_begin_events(self):
0069         cursor = 0
0070         while self.__dot_lines[cursor].split()[0] != "{node":
0071            cursor += 1
0072         while self.__dot_lines[cursor].split()[0] == "{node":
0073            cursor += 1
0074         # skip initial state transition
0075         cursor += 1
0076         return cursor
0077
0078     def __get_state_variables(self):
0079         # wait for node declaration
0080         states = []
0081         final_states = []
0082
0083         has_final_states = False
0084         cursor = self.__get_cursor_begin_states()
0085
0086         # process nodes
0087         while self.__dot_lines[cursor].split()[0] == "{node":
0088             line = self.__dot_lines[cursor].split()
0089             raw_state = line[-1]
0090
0091             #  "enabled_fired"}; -> enabled_fired
0092             state = raw_state.replace('"', '').replace('};', '').replace(',','_')
0093             if state[0:7] == "__init_":
0094                 initial_state = state[7:]
0095             else:
0096                 states.append(state)
0097                 if self.__dot_lines[cursor].__contains__("doublecircle") == True:
0098                     final_states.append(state)
0099                     has_final_states = True
0100
0101                 if self.__dot_lines[cursor].__contains__("ellipse") == True:
0102                     final_states.append(state)
0103                     has_final_states = True
0104
0105             cursor += 1
0106
0107         states = sorted(set(states))
0108         states.remove(initial_state)
0109
0110         # Insert the initial state at the bein og the states
0111         states.insert(0, initial_state)
0112
0113         if has_final_states == False:
0114             final_states.append(initial_state)
0115
0116         return states, initial_state, final_states
0117
0118     def __get_event_variables(self):
0119         # here we are at the begin of transitions, take a note, we will return later.
0120         cursor = self.__get_cursor_begin_events()
0121
0122         events = []
0123         while self.__dot_lines[cursor][1] == '"':
0124             # transitions have the format:
0125             # "all_fired" -> "both_fired" [ label = "disable_irq" ];
0126             #  ------------ event is here ------------^^^^^
0127             if self.__dot_lines[cursor].split()[1] == "->":
0128                 line = self.__dot_lines[cursor].split()
0129                 event = line[-2].replace('"','')
0130
0131                 # when a transition has more than one lables, they are like this
0132                 # "local_irq_enable\nhw_local_irq_enable_n"
0133                 # so split them.
0134
0135                 event = event.replace("\\n", " ")
0136                 for i in event.split():
0137                     events.append(i)
0138             cursor += 1
0139
0140         return sorted(set(events))
0141
0142     def __create_matrix(self):
0143         # transform the array into a dictionary
0144         events = self.events
0145         states = self.states
0146         events_dict = {}
0147         states_dict = {}
0148         nr_event = 0
0149         for event in events:
0150             events_dict[event] = nr_event
0151             nr_event += 1
0152
0153         nr_state = 0
0154         for state in states:
0155             states_dict[state] = nr_state
0156             nr_state += 1
0157
0158         # declare the matrix....
0159         matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
0160
0161         # and we are back! Let's fill the matrix
0162         cursor = self.__get_cursor_begin_events()
0163
0164         while self.__dot_lines[cursor][1] == '"':
0165             if self.__dot_lines[cursor].split()[1] == "->":
0166                 line = self.__dot_lines[cursor].split()
0167                 origin_state = line[0].replace('"','').replace(',','_')
0168                 dest_state = line[2].replace('"','').replace(',','_')
0169                 possible_events = line[-2].replace('"','').replace("\\n", " ")
0170                 for event in possible_events.split():
0171                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
0172             cursor += 1
0173
0174         return matrix