tools/verification/dot2/automata.py

   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
  11 import ntpath
  12
  13 class 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 basename.endswith(".dot") == False:
  33             print("not a dot file")
  34             raise Exception("not a dot file: %s" % self.__dot_path)
  35
  36         model_name = basename[0:-4]
  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 self.__dot_lines[cursor].__contains__("doublecircle") == True:
  98                     final_states.append(state)
  99                     has_final_states = True
 100
 101                 if self.__dot_lines[cursor].__contains__("ellipse") == True:
 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 has_final_states == False:
 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][1] == '"':
 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][1] == '"':
 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