verification/dot2/dot2c.py

25     def __init__(self, file_path):
27         self.line_length = 100
29     def __buff_to_string(self, buff):
38     def __get_enum_states_content(self):
40         buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix))
41         for state in self.states:
42             if state != self.initial_state:
43                 buff.append("\t%s%s," % (state, self.enum_suffix))
44         buff.append("\tstate_max%s" % (self.enum_suffix))
48     def get_enum_states_string(self):
49         buff = self.__get_enum_states_content()
50         return self.__buff_to_string(buff)
52     def format_states_enum(self):
54         buff.append("enum %s {" % self.enum_states_def)
55         buff.append(self.get_enum_states_string())
60     def __get_enum_events_content(self):
63         for event in self.events:
65                 buff.append("\t%s%s = 0," % (event, self.enum_suffix))
68                 buff.append("\t%s%s," % (event, self.enum_suffix))
70         buff.append("\tevent_max%s" % self.enum_suffix)
74     def get_enum_events_string(self):
75         buff = self.__get_enum_events_content()
76         return self.__buff_to_string(buff)
78     def format_events_enum(self):
80         buff.append("enum %s {" % self.enum_events_def)
81         buff.append(self.get_enum_events_string())
86     def get_minimun_type(self):
89         if self.states.__len__() > 255:
92         if self.states.__len__() > 65535:
95         if self.states.__len__() > 1000000:
96             raise Exception("Too many states: %d" % self.states.__len__())
100     def format_automaton_definition(self):
101         min_type = self.get_minimun_type()
103         buff.append("struct %s {" % self.struct_automaton_def)
104         buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
105         buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
106         buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix))
108         buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
112     def format_aut_init_header(self):
114         buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
117     def __get_string_vector_per_line_content(self, buff):
130     def get_aut_init_events_string(self):
131         return self.__get_string_vector_per_line_content(self.events)
133     def get_aut_init_states_string(self):
134         return self.__get_string_vector_per_line_content(self.states)
136     def format_aut_init_events_string(self):
139         buff.append(self.get_aut_init_events_string())
143     def format_aut_init_states_string(self):
146         buff.append(self.get_aut_init_states_string())
151     def __get_max_strlen_of_states(self):
152         max_state_name = max(self.states, key = len).__len__()
153         return max(max_state_name, self.invalid_state_str.__len__())
155     def __get_state_string_length(self):
156         maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__()
159     def get_aut_init_function(self):
160         nr_states = self.states.__len__()
161         nr_events = self.events.__len__()
164         strformat = self.__get_state_string_length()
169                 next_state = self.function[x][y]
170                 if next_state != self.invalid_state_str:
171                     next_state = self.function[x][y] + self.enum_suffix
179         return self.__buff_to_string(buff)
181     def format_aut_init_function(self):
184         buff.append(self.get_aut_init_function())
189     def get_aut_init_initial_state(self):
190         return self.initial_state
192     def format_aut_init_initial_state(self):
194         initial_state = self.get_aut_init_initial_state()
195         buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")
199     def get_aut_init_final_states(self):
202         for state in self.states:
208             if self.final_states.__contains__(state):
214     def format_aut_init_final_states(self):
216        buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
220     def __get_automaton_initialization_footer_string(self):
224     def format_aut_init_footer(self):
226         buff.append(self.__get_automaton_initialization_footer_string())
230     def format_invalid_state(self):
232         buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix))
236     def format_model(self):
238         buff += self.format_states_enum()
239         buff += self.format_invalid_state()
240         buff += self.format_events_enum()
241         buff += self.format_automaton_definition()
242         buff += self.format_aut_init_header()
243         buff += self.format_aut_init_states_string()
244         buff += self.format_aut_init_events_string()
245         buff += self.format_aut_init_function()
246         buff += self.format_aut_init_initial_state()
247         buff += self.format_aut_init_final_states()
248         buff += self.format_aut_init_footer()
252     def print_model_classic(self):
253         buff = self.format_model()
254         print(self.__buff_to_string(buff))