improved dot generation

analyze.py

@@ -56,6 +56,7 @@ if __name__ == "__main__":
     #ast = parse_file(args.filename, use_cpp=False)
     #ast.show()
 
+    initial_state = args.initial
     assign_table = []
     state_enums = []
     func_table = {}
@@ -129,12 +130,15 @@ if __name__ == "__main__":
     print("States: ", ",".join(states))
     print("")
     
+    reachable_states = [initial_state]
     props_by_state = {}
     print("Compact Transition Table:")
     for n,ms in comp_tt.items():
         sstr = ','.join(ms)
         print(f"{n}->{{{sstr}}}")
-
+        for s in ms:
+            if not(s in reachable_states):
+                reachable_states.append(s)
         # find properties
         for f in fsm_funcs:
             sccpv = SwitchCaseCodePropertyVisitor(n, pure_sa)
@@ -143,18 +147,28 @@ if __name__ == "__main__":
                 props_by_state[n] = sccpv.properties
     print("")
 
-    properties = {}
+    print("Reachable States")
+
+    states_by_property = {}
     for state,props in props_by_state.items():
         for prop in props:
-            if prop in properties:
+            if prop in states_by_property:
-                properties[prop].append(state)
+                states_by_property[prop].append(state)
             else:
-                properties[prop] = [state]
+                states_by_property[prop] = [state]
+    
+    properties = {}
+    property_alias = {}
+    for i,(prop,pstates) in enumerate(states_by_property.items()):
+        print("foo ", i)
+        alias = base_10_to_alphabet(i + 1)
+        property_alias[prop] = alias
+        properties[alias] = (pstates, prop)
 
     print("Properties")
-    for prop,pstates in properties.items():
+    for prop,(pstates,full_prop) in properties.items():
         ss = ','.join(pstates)
-        print(f" - '{prop}' when {ss}")
+        print(f" - '{full_prop}' when {ss}")
     print("")
 
     ltls = []
@@ -163,7 +177,7 @@ if __name__ == "__main__":
             ltls = [line.rstrip() for line in f]
     
     
-    mod = ModelBuilder(states, args.initial, comp_tt, properties, ltls=ltls)
+    mod = ModelBuilder(reachable_states, initial_state, comp_tt, properties, ltls=ltls)
     nusmv = mod.generate()
 
     if args.output is not None:
@@ -175,15 +189,16 @@ if __name__ == "__main__":
     
     if args.dot is not None:
         g = gv.Digraph('G')
-        
+        print(props_by_state)
+        print(property_alias)
         for state in states:
             shape = 'circle'
-            if state == args.initial:
+            if state == initial_state:
                 shape = 'doublecircle'
 
             if state in props_by_state:
-                pstr = ",".join(props_by_state[state])
+                pstr = ",".join([property_alias[x] for x in props_by_state[state]])
-                g.node(state, label=state, xlabel=f"{{{pstr}}}", shape=shape)
+                g.node(state, label=f"{state}\n\n{{{pstr}}}", shape=shape)
             else:
                 g.node(state, label=state, shape=shape)
               

modelbuilder.py

@@ -26,31 +26,6 @@ LTL_FORM = """LTLSPEC
     {ltl};
 """
 
-A_UPPERCASE = ord('a')
-ALPHABET_SIZE = 26
-
-
-def _decompose(number):
-    """Generate digits from `number` in base alphabet, least significants
-    bits first.
-
-    Since A is 1 rather than 0 in base alphabet, we are dealing with
-    `number - 1` at each iteration to be able to extract the proper digits.
-    """
-
-    while number:
-        number, remainder = divmod(number - 1, ALPHABET_SIZE)
-        yield remainder
-
-
-def base_10_to_alphabet(number):
-    """Convert a decimal number to its base alphabet representation"""
-
-    return ''.join(
-            chr(A_UPPERCASE + part)
-            for part in _decompose(number)
-    )[::-1]
-
 class ModelBuilder:
     def __init__(self, states, initial, transitions, properties, ltls=[], name="main"):
         self._name = name
@@ -60,10 +35,6 @@ class ModelBuilder:
         self._props = properties
         self._ltls = ltls
 
-        self._propalias = {}
-        for no,prop in enumerate(properties.keys()):
-            self._propalias[prop] = base_10_to_alphabet(no + 1)
-
     def generate(self):
         # build model
         states_decl = ",".join(self._states)
@@ -74,8 +45,7 @@ class ModelBuilder:
             transitions.append(transition)
 
         properties = []
-        for prop,states in self._props.items():
+        for alias,(states,prop) in self._props.items():
-            alias = self._propalias[prop]
             logic = " | ".join([PROP_LOGIC.format(state=x) for x in states])
             prop_str = PROP.format(prop=prop, alias=alias, logic=logic)
             properties.append(prop_str)

utils.py

@@ -1,5 +1,30 @@
 import re
 
+A_UPPERCASE = ord('a')
+ALPHABET_SIZE = 26
+
+
+def _decompose(number):
+    """Generate digits from `number` in base alphabet, least significants
+    bits first.
+
+    Since A is 1 rather than 0 in base alphabet, we are dealing with
+    `number - 1` at each iteration to be able to extract the proper digits.
+    """
+
+    while number:
+        number, remainder = divmod(number - 1, ALPHABET_SIZE)
+        yield remainder
+
+
+def base_10_to_alphabet(number):
+    """Convert a decimal number to its base alphabet representation"""
+
+    return ''.join(
+            chr(A_UPPERCASE + part)
+            for part in _decompose(number)
+    )[::-1]
+
 def find_longest_path(paths):
     ms = 0
     mp = None