LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2022 Dominic Hoeglinger.
+Copyright (c) 2022 flip. 
 
 Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
 

analyze.py

@@ -1,44 +1,21 @@
 from __future__ import print_function
 import argparse
 import os,sys,io
-from pycparser import parse_file, c_ast, CParser, c_generator
+from pycparser import parse_file, c_ast, CParser
 from pcpp import Preprocessor
 import graphviz as gv
-import html
-from dataclasses import dataclass
 
 from modelbuilder import *
 from utils import *
 from astvisitors import *
 
-def parse_statevar(statevar):
-    r_struct = r'(\w+)(\.|->)(\w+)'
-    match = re.match(r_struct, statevar)
-    if match:
-        name,typ,field = match.groups()
-        return c_ast.StructRef(c_ast.ID(name), typ, c_ast.ID(field))
-    return c_ast.ID(statevar)
-
-@dataclass
-class PathAssignment:
-    lvalue:c_ast.Node
-    rvalue:c_ast.Node
-    condition:c_ast.Node
-
 if __name__ == "__main__":
     argparser = argparse.ArgumentParser('Create a Kripke Structure Model from C Code')
     argparser.add_argument('filename',
                            nargs='?',
                            help='name of file to parse')
-
-    argparser.add_argument('-I', '--includedirs', nargs='+', default=[])
-    argparser.add_argument('-D', '--defines', nargs='+', default=[])
-    argparser.add_argument('-p', '--preprocess', help='output preprocessor file')
-    argparser.add_argument('-c', '--conditional', help='only count state assignment if this conditional applies on the path')
-    argparser.add_argument('--inputids', nargs='+', default=[])
     argparser.add_argument('--func', help='process function')
     argparser.add_argument('--enum', help='state enum')
-    argparser.add_argument('--statevar', help='state variable')
     argparser.add_argument('--initial', help='initial state')
     argparser.add_argument('--ltlfile', help='file containing LTL formulae')
     argparser.add_argument('-o', '--output', dest='output', help='output NuSMV file')
@@ -52,293 +29,131 @@ if __name__ == "__main__":
     
     p = Preprocessor()
     p.add_path('/usr/lib/gcc/x86_64-linux-gnu/12/include/')
-    for inc in args.includedirs:
-        #print(f"Include-Dir: {inc}")
-        p.add_path(inc)
-    
-    for define in args.defines:
-        name,value = define.split('=')
-        #print(f"Define: {name}={value}")
-        p.define(f"{name} {value}")
 
     p.parse(source)
     oh = io.StringIO()
     p.write(oh)
     prep_source = oh.getvalue()
     
-    if args.preprocess is not None:
-        with open(args.preprocess, "wt") as f:
-            n = f.write(prep_source)
-    
-    cg = CGenerator()
-    
+    #print(prep_source)
+    #exit()
+
     parser = CParser()
     ast = parser.parse(prep_source)
-    ass = parse_statevar(args.statevar)
-    tg = TypedefGatherer()
-    tg.visit(ast)
-    typedefs = tg.typedefs
-    #print("Typedefs", typedefs.keys())
+    #ast = parse_file(args.filename, use_cpp=False)
     
-    tast = TypedIdTransformer(typedefs).transform(ast)
-    #tast.show()
-    ast = tast
-
-    initial_state = args.initial
     assign_table = []
     state_enums = []
     func_table = {}
     enum_table = {}
     state_asmts = []
-    fsm_funcs = []
-    tran_table = []
-    properties = []
     
-    def get_rightmost_field(node):
-        if isinstance(node, c_ast.StructRef):
-            return get_rightmost_field(node.field)
-        return node
-    state_id = get_rightmost_field(ass).name
-    
-    #TMR
-    #input_ids = ['m_bIn', 'm_ulActTime']
-    #SLM
-    input_ids = ['m_bEnable', 'm_bCondition', 'm_ucEnableUnconditioned']
-    #conditional_ids = [*input_ids, 'm_ucTimerType']
-    input_ids = args.inputids
-
     fdv = FuncDefVisitor()
     fdv.visit(ast)
     func_table = fdv.func_table
-    proc_func = None
-    if not(args.func in func_table):
-        raise Exception(f"Function name '{args.func}' not found!")
-    else:
-        proc_func = func_table[args.func]
-    
-    fast = AstFuncCallInlinerTransformer(func_table).transform(ast)
-    ast = fast
 
     etv = EnumTypedefVisitor()
     etv.visit(ast)
     enum_table = etv.enums
-    states = []
     
-    # Update ProcFunc to unrolled form - TODO
-    fdv = FuncDefVisitor()
-    fdv.visit(ast)
-    func_table = fdv.func_table
-    proc_func = None
     if not(args.func in func_table):
         raise Exception(f"Function name '{args.func}' not found!")
-    else:
-        proc_func = func_table[args.func]
 
-    def discover_cals(func):
-        funcs = []
-        child_funcs = []
-        fcv = FuncCallVisitor()
-        fcv.visit(func)
-        for fc in fcv.func_calls:
-            if fc in func_table:
-                funcs.append(func_table[fc])
-                child_funcs += discover_cals(func_table[fc])
-        return funcs + child_funcs
-
-    # discover FSM functions
-    fsm_funcs.append(proc_func)
-    fsm_funcs += discover_cals(proc_func)
-    #fsm_funcs += [ func_table[x] for x in fcv.func_calls ]
-    
-    print("Function Table")
-    for f in fsm_funcs:
-        print(f" - {f.decl.name} {'<<< entry' if (f.decl.name == args.func) else ''}")
-    print("")
-
-    config_cond = None
-    cond_blacklist = []
-    cond_whitelist = []
-    if args.conditional is not None:
-        config_cond = args.conditional
-        print(f"Configuration Conditional {config_cond}")
-        config_type = None
-        config_enums = None
-        for name,enum_type in enum_table.items():
-            ev = EnumVisitor()
-            ev.visit(enum_type)
-            if config_cond in ev.enum_names:
-                config_type = name
-                config_enums = ev.enum_names
-                break
-        if config_type is not None:
-            print(f" - Type is {config_type}")
-            cond_whitelist.append(config_cond)
-            print( " - Enum Blacklist is")
-            for enum in config_enums:
-                if enum != config_cond:
-                    print(f"   * {enum}")
-                    cond_blacklist.append(enum)
-        else:
-            print("No type found for conditional, ignoring")
-        print("")
-
-    print("Enum Table")
     if args.enum in enum_table:
         ev = EnumVisitor()
         ev.visit(enum_table[args.enum])
         for ename in ev.enum_names:
-            print(" - ",ename)
-            states.append(ename)
+            sav = StateAssignmentVisitor(ename)
+            sav.visit(func_table[args.func])
+            state_asmts += sav.assignments
     else:
         print(f"Initial State Enum '{args.enum}' not found")
+
+    paths = []
+    for asm in state_asmts:
+        paths.append(asm[1])
+
+    common = find_common_ancestor(paths)
+
+    tran_table = []
+
+    for sa in state_asmts:
+        sctv = SwitchCaseTranVisitor(sa[0])
+        sctv.visit(common)
+        tran_table += sctv.tran_table
+
+    comp_tt = {}
+    print("Transitions")
+    for t in tran_table:
+        print(f"{t[0]}->{t[1]}")
+        if t[0] in comp_tt:
+            comp_tt[t[0]].append(t[1])
+        else:
+            comp_tt[t[0]] = [t[1]]
     print("")
 
-    print("Extracting State Transitions")
-    sav = StateAssignmentVisitor(func_table, ass)
-    sav.visit(proc_func)
-    for assignment in sav.assignments:
-        state_to = assignment.state
-        cpa = ConditionalPathAnalyzer()
-        #print("Path", path_to_str(assignment.path))
-        cpa.analyze(reversed(assignment.path))
-        cond_chain = []
-        conds_state = []
-        state_from_expr = None
-        disregard_transition = False
-        for c in cpa.condition_chain:
-            # filter by conditional enum
-            # this is far from correct
-            cond_blacklist_visitor = ContainsOneOfIdVisitor(cond_blacklist)
-            cond_blacklist_visitor.visit(c)
-            if cond_blacklist_visitor.hit:
-                disregard_transition = True
-                break
-            conditional_visitor = ContainsOneOfIdVisitor(input_ids)
-            conditional_visitor.visit(c)
-            if conditional_visitor.hit:
-                cond_chain.append(c)
-            state_condition_visitor = ContainsOneOfIdVisitor([state_id])
-            state_condition_visitor.visit(c)
-            if state_condition_visitor.hit:
-                conds_state.append(c)
-
-        if not(disregard_transition):
-            if len(conds_state) != 1:
-                cond_exprs = [cg.visit(x) for x in cpa.condition_chain]
-                print("OOPS")
-                print(cond_exprs, conds_state)
-                raise Exception("No or too many state conditions found")
-            # find out from which state the assignment transitions
-            current_state_visitor = ContainsOneOfIdVisitor(states)
-            current_state_visitor.visit(conds_state[0])
-            if not(current_state_visitor.hit):
-                raise Exception("State assignment does not assign state enum")
-            state_from = current_state_visitor.name
-            condition = None
-            if len(cond_chain) == 1:
-                condition = cond_chain[0]
-            elif len(cond_chain) > 1:
-                condition = cond_chain[0]
-                for expr in cond_chain[1:len(cond_chain)]:
-                    condition = c_ast.BinaryOp('&&', expr, condition)
-                
-            cond_exprs = [cg.visit(x) for x in cond_chain]
-            cond_expr = cg.visit(condition)
-            
-            tf = NuSmvConditionTransformer()
-            cond_mod = tf.transform(condition)
-            mod_expr = cg.visit(cond_mod)
-            if cond_mod is None:
-                print(f" - {state_from} -> {state_to} unconditional")
-            else:
-                print(f" - {state_from} -> {state_to} on {mod_expr}")
-            tran_table.append(StateTransition(state_from, state_to, condition))
+    pure_sa = [x[0] for x in state_asmts]
+    states = comp_tt.keys()
+    print("States: ", ",".join(states))
     print("")
 
+    props_by_state = {}
+    print("Compact Transition Table:")
+    for n,ms in comp_tt.items():
+        sstr = ','.join(ms)
+        print(f"{n}->{{{sstr}}}")
 
-    # Extract properties
-    av = AssignmentVisitor(func_table)
-    av.visit(proc_func)
-    path_assigments = []
-    
-    for a in av.assignments:
-        if a.node.op == '=':
-            if isinstance(a.node.lvalue, c_ast.StructRef):
-                if not(check_structref_equivalence(a.node.lvalue, ass)):
-                    path_assigments.append(a)
-    assignments = {}
-    for a in path_assigments:
-        cpa = ConditionalPathAnalyzer()
-        #print("Path", path_to_str(assignment.path))
-        cpa.analyze(reversed(a.path))
-        cond_chain = []
-        conds_state = []
-        state_from_expr = None
-        disregard_assignment = False
-        for c in cpa.condition_chain:
-            # filter by conditional enum
-            # this is far from correct
-            cond_blacklist_visitor = ContainsOneOfIdVisitor(cond_blacklist)
-            cond_blacklist_visitor.visit(c)
-            if cond_blacklist_visitor.hit:
-                disregard_assignment = True
-                break
-            conditional_visitor = ContainsOneOfIdVisitor(input_ids)
-            conditional_visitor.visit(c)
-            if conditional_visitor.hit:
-                cond_chain.append(c)
-            state_condition_visitor = ContainsOneOfIdVisitor([state_id])
-            state_condition_visitor.visit(c)
-            if state_condition_visitor.hit:
-                conds_state.append(c)
+        # find properties
+        sccpv = SwitchCaseCodePropertyVisitor(n, pure_sa)
+        sccpv.visit(common)
+        if len(sccpv.properties) > 0:
+            props_by_state[n] = sccpv.properties
+    print("")
 
-        if not(disregard_assignment):
-            conds_state_tf = []
-            # transform state conditions to output format
-            for state_cond in conds_state:
-                current_state_visitor = ContainsOneOfIdVisitor(states)
-                current_state_visitor.visit(conds_state[0])
-                if not(current_state_visitor.hit):
-                    raise Exception("State assignment does not assign state enum")
-                state_from = current_state_visitor.name
-                conds_state_tf.append(c_ast.BinaryOp('==', c_ast.ID("state"), c_ast.ID(state_from)))
-            conds_state = conds_state_tf
-            state_cond = None
-            condition = None
-            if len(conds_state) == 1:
-                state_cond = conds_state[0]
-            elif len(conds_state) > 1:
-                state_cond = conds_state[0]
-                for expr in cond_chain[1:len(conds_state)]:
-                    condition = c_ast.BinaryOp('||', expr, state_cond)
-            
-            if len(cond_chain) == 1:
-                condition = cond_chain[0]
-            elif len(cond_chain) > 1:
-                condition = cond_chain[0]
-                for expr in cond_chain[1:len(conds_state)]:
-                    condition = c_ast.BinaryOp('&&', expr, condition)
-            
-            if condition is None and state_cond is not None:
-                condition = state_cond
-            elif condition is not None and state_cond is not None:
-                condition = c_ast.BinaryOp('&&', condition, state_cond)
-            
-            cond_exprs = cg.visit(condition)
-            #state_cond_exprs = cg.visit(state_cond)
-            variable = cg.visit(NuSmvConditionTransformer().transform(a.node.lvalue))
-            if variable in assignments:
-                assignments[variable].append(PathAssignment(a.node.lvalue, a.node.rvalue, condition))
+    properties = {}
+    for state,props in props_by_state.items():
+        for prop in props:
+            if prop in properties:
+                properties[prop].append(state)
             else:
-                assignments[variable] = [PathAssignment(a.node.lvalue, a.node.rvalue, condition)]
-            #print(f" - {cg.visit(a.node)} {cond_exprs}")
+                properties[prop] = [state]
     
-    print("Assignments")
-    for var,assigns in assignments.items():
-        print(f" - {var}")
-        for assign in assigns:
-            print(f"   -> '{cg.visit(assign.rvalue)}' on {cg.visit(assign.condition)}")
+    print("Properties")
+    for prop,pstates in properties.items():
+        ss = ','.join(pstates)
+        print(f" - '{prop}' when {ss}")
+    print("")
 
-    mod = ModelBuilder(states, initial_state, tran_table, assignments)
+    ltls = []
+    if args.ltlfile is not None:
+        with open(args.ltlfile) as f:
+            ltls = [line.rstrip() for line in f]
+
+
+    mod = ModelBuilder(states, args.initial, comp_tt, properties, ltls=ltls)
     nusmv = mod.generate()
-    print(nusmv)
+
+    if args.output is not None:
+        with open(args.output, "wt") as f:
+            n = f.write(nusmv)
+    else:
+        print("-------------------")
+        print(nusmv)
+    
+    if args.dot is not None:
+        g = gv.Digraph('G')
+        
+        for state in states:
+            if state in props_by_state:
+                pstr = ",".join(props_by_state[state])
+                if state == args.initial:
+                    g.attr('node', shape='doublecircle')
+                else:
+                    g.attr('node', shape='circle')
+                g.node(state, label=state, xlabel=f"{{{pstr}}}")
+              
+                
+        
+        for t in tran_table:
+            g.edge(t[0], t[1])
+        g.render(filename=args.dot)

astvisitors.py

@@ -1,24 +1,46 @@
-import re
-from pycparser import c_ast, c_generator
-from itertools import pairwise
-from dataclasses import dataclass
-
-def path_to_str(p):
-    return "->".join([str(n.__class__.__name__) for n in p])
+from pycparser import c_ast
 
 class FuncDefVisitor(c_ast.NodeVisitor):
     def __init__(self):
         self.func_table = {}
-
     def visit_FuncDef(self, node):
         self.func_table[node.decl.name] = node
 
-class FuncCallVisitor(c_ast.NodeVisitor):
-    def __init__(self):
-        self.func_calls = []
+class StateAssignmentVisitor(c_ast.NodeVisitor):
+    def __init__(self, state):
+        super().__init__()
+        self.state = state
+        self.assignments = []
 
-    def visit_FuncCall(self, node):
-        self.func_calls.append(node.children()[0][1].name)
+    def visit(self, node, path = None):
+        """ Visit a node.
+        """
+        if path is None:
+            path = []
+        if self._method_cache is None:
+            self._method_cache = {}
+
+        visitor = self._method_cache.get(node.__class__.__name__, None)
+        if visitor is None:
+            method = 'visit_' + node.__class__.__name__
+            visitor = getattr(self, method, self.generic_visit)
+            self._method_cache[node.__class__.__name__] = visitor
+
+        return visitor(node, path)
+
+    def generic_visit(self, node, path):
+        """ Called if no explicit visitor function exists for a
+            node. Implements preorder visiting of the node.
+        """
+        path = path.copy()
+        path.append(node)
+        for c in node:
+            self.visit(c, path)
+
+    def visit_Assignment(self, n, path):
+        rval_str = n.rvalue.name
+        if rval_str == self.state:
+            self.assignments.append((n,path))
 
 class EnumDefVisitor(c_ast.NodeVisitor):
     def __init__(self, name):
@@ -47,581 +69,56 @@ class EnumVisitor(c_ast.NodeVisitor):
     def visit_Enumerator(self, node):
         self.enum_names.append(node.name)        
 
-class PathVisitor(object):
-    def __init__(self):
-        self._method_cache = {}
-
-    def visit(self, node, path = None):
-        if path is None:
-            path = []
-
-        visitor = self._method_cache.get(node.__class__.__name__, None)
-        if visitor is None:
-            method = 'visit_' + node.__class__.__name__
-            visitor = getattr(self, method, self.generic_visit)
-            self._method_cache[node.__class__.__name__] = visitor
-
-        return visitor(node, path)
-    
-    def generic_visit(self, node, path):
-        path = path.copy()
-        path.append(node)
-        for c in node:
-            self.visit(c, path)
-
-class FuncCallDeferPathVisitor(PathVisitor):
-    def __init__(self, func_table):
+class SwitchCaseTermVisitor(c_ast.NodeVisitor):
+    def __init__(self, asm_node):
         super().__init__()
-        self.func_table = func_table
-    
-    def visit_FuncCall(self, node, path):
-        fcall = node.name.name
-        if fcall in self.func_table:
-            self.visit(self.func_table[fcall], path)
-
-def check_node_equivalence(lhs, rhs):
-    return str(lhs) == str(rhs)
-
-def check_structref_equivalence(lhs:c_ast.StructRef, rhs:c_ast.StructRef):
-    if lhs.name.name != rhs.name.name:
-        return False
-    if lhs.field.name != rhs.field.name:
-        return False
-    return True
-
-@dataclass
-class PathStateAssignment:
-    path:list[c_ast.Node]
-    node:c_ast.Assignment
-    state:str
-
-class StateAssignmentVisitor(FuncCallDeferPathVisitor):
-    def __init__(self, func_table, variable):
-        super().__init__(func_table)
-        self.variable = variable
-        self.assignments = []
-
-    def visit_Assignment(self, n, path):
-        if check_structref_equivalence(self.variable, n.lvalue):
-            if isinstance(n.rvalue, c_ast.ID):
-                self.assignments.append(PathStateAssignment(path, n, n.rvalue.name))
-            elif isinstance(n.rvalue, c_ast.TernaryOp):
-                #print("TOP", n.rvalue)
-                pass
-        
-
-@dataclass
-class PathAssignment:
-    path:list[c_ast.Node]
-    node:c_ast.Assignment
-
-class AssignmentVisitor(FuncCallDeferPathVisitor):
-    def __init__(self, func_table):
-        super().__init__(func_table)
-        self.assignments = []
-
-    def visit_Assignment(self, n, path):
-        self.assignments.append(PathAssignment(path, n))
-        
-
-class PathAnalyzer(object):
-    def __init__(self):
-        self._method_cache = {}
-
-    def analyze(self, path):
-        trace = []
-        for node in path:
-            self._invoke_visitor(node, trace)
-            trace.append(node)
-
-    def _invoke_visitor(self, node, trace):
-        visitor = self._method_cache.get(node.__class__.__name__, None)
-        if visitor is None:
-            method = 'visit_' + node.__class__.__name__
-            visitor = getattr(self, method, None)
-            self._method_cache[node.__class__.__name__] = visitor
-
-        if visitor is not None:
-            visitor(node, trace)
-
-@dataclass
-class GeneralizedCase:
-    exprs:list[c_ast.Node]
-    stmts:list[c_ast.Node]
-
-class ConditionalPathAnalyzer(PathAnalyzer):
-    def __init__(self):
-        super().__init__()
-        self.condition_chain = []
-
-    def visit_If(self, node, trace):
-        p = trace[-1]
-        #print("If", node)
-        if node.iftrue == p:
-            #print("->iftrue")
-            self.condition_chain.append(node.cond)
-        elif node.iffalse == p:
-            #print("->iffalse")
-            neg = c_ast.UnaryOp('!', node.cond)
-            self.condition_chain.append(neg)
-        else:
-            pass
-
-    def visit_Switch(self, node, trace):
-        p_case = trace[-2]
-        expr_fallthrough = []
-        gencases = []
-        cond = node.cond
-        block_items = node.stmt.block_items
-        parent_case_idx = None
-        #print("Switch", cond)
-        #print("P:", p_case)
-        #print("CI", block_items)
-        # lump together fallthrough cases
-        for case in block_items:
-            if p_case == case:
-                parent_case_idx = len(gencases)
-            if not isinstance(case, c_ast.Default):
-                expr_fallthrough.append(case.expr)
-                if len(case.stmts) != 0 and isinstance(case.stmts[-1], c_ast.Break):
-                    gencases.append(GeneralizedCase(expr_fallthrough, case.stmts))
-                    expr_fallthrough = []
-        #print("Generalized P-Case", gencases[parent_case_idx].exprs)
-        # does not account for default, which needs the entire set of cases
-        # checked for unequals and and-ed
-        eqops = [c_ast.BinaryOp('==', cond, expr) for expr in gencases[parent_case_idx].exprs]
-        if len(eqops) == 1:
-            self.condition_chain.append(eqops[0])
-        elif len(eqops) > 1:
-            orop = eqops[0]
-            for expr in eqops[1:len(eqops)]:
-                orop = c_ast.BinaryOp('||', expr, orop)
-            self.condition_chain.append(orop)
-        else:
-            raise Exception("Unexpected number of expressions")
-
-class ContainsOneOfIdVisitor(c_ast.NodeVisitor):
-    def __init__(self, ids):
-        self.ids = ids
+        self._asm_node = asm_node
         self.hit = False
-        self.name = None
 
-    def visit_ID(self, node):
-        if node.name in self.ids:
+    def visit_Assignment(self, node):
+        if node == self._asm_node:
             self.hit = True
-            self.name = node.name
 
-    def visit_TypedID(self, node):
-        return self.visit_ID(node)
-
-@dataclass
-class StateTransition:
-    state_from:str
-    state_to:str
-    condition:c_ast.Node
-
-class TypedefGatherer(c_ast.NodeVisitor):
-    def __init__(self):
-        self.typedefs = {}
-
-    def visit_Typedef(self, node):
-        self.typedefs[node.name] = node
-
-
-class AstTransformer(object):
-    def __init__(self):
-        self._method_cache = {}
-
-    def transform(self, node):
-        visitor = self._method_cache.get(node.__class__.__name__, None)
-        if visitor is None:
-            method = 'transform_' + node.__class__.__name__
-            visitor = getattr(self, method, self._transform_generic)
-            self._method_cache[node.__class__.__name__] = visitor
-        
-        return visitor(node)
-
-    def _transform_Node(self, node):
-        new_c = []
-        for c_name in node.__slots__[0:-1]:
-            c = getattr(node, c_name)
-            new_c.append(self.transform(c))
-        node_constructor = node.__class__
-        return node_constructor(*new_c)
-
-    def _transform_generic(self, node):
-        if isinstance(node, c_ast.Node):
-            return self._transform_Node(node)
-        elif isinstance(node, list):
-            return [self.transform(x) for x in node]
-        else:
-            return node
-
-class AstPathTransformer(object):
-    def __init__(self):
-        self._method_cache = {}
-
-    def transform(self, node, path = None):
-        if path is None:
-            path = [node]
-        else:
-            path = path.copy()
-            path.append(node)
-
-        visitor = self._method_cache.get(node.__class__.__name__, None)
-        if visitor is None:
-            method = 'transform_' + node.__class__.__name__
-            visitor = getattr(self, method, self._transform_generic)
-            self._method_cache[node.__class__.__name__] = visitor
-        
-        return visitor(node, path)
-
-    def _transform_Node(self, node, path):
-        new_c = []
-        for c_name in node.__slots__[0:-1]:
-            c = getattr(node, c_name)
-            new_c.append(self.transform(c, path))
-        node_constructor = node.__class__
-        return node_constructor(*new_c)
-
-    def _transform_generic(self, node, path):
-        if isinstance(node, c_ast.Node):
-            return self._transform_Node(node, path)
-        elif isinstance(node, list):
-            return [self.transform(x, path) for x in node]
-        else:
-            return node
-
-
-
-class TypedID(c_ast.ID):
-    __slots__ = ('name', 'type', 'coord')
-    def __init__(self, name, type=None, coord=None):
-        super().__init__(name, coord)
-        self.type = type
-
-    def children(self):
-        nodelist = []
-        return tuple(nodelist)
-
-    def __iter__(self):
-        return
-        yield
-
-    attr_names = ('name', 'type' )
-
-class CGenerator(c_generator.CGenerator):
-    def __init__(self):
+class SwitchCaseTranVisitor(c_ast.NodeVisitor):
+    def __init__(self, asm_node):
         super().__init__()
-    
-    def visit_TypedID(self, n):
-        return n.name
+        self._asm_node = asm_node
+        self.tran_table = []
 
+    def visit_Case(self, node):
+        sctv = SwitchCaseTermVisitor(self._asm_node)
+        sctv.visit(node)
+        if sctv.hit:
+            self.tran_table.append((node.children()[0][1].name, self._asm_node.rvalue.name))
 
-class TypeDeclFinder(c_ast.NodeVisitor):
-    def __init__(self, declname):
-        self.declname = declname
-        self.decl = None
-
-    def visit_TypeDecl(self, node):
-        if node.declname == self.declname:
-            self.decl = node
-
-class DeclFinder(c_ast.NodeVisitor):
-    def __init__(self, declname):
-        self.declname = declname
-        self.decl = None
-
-    def visit_Decl(self, node):
-        if node.name == self.declname:
-            self.decl = node
-
-class IdentifierTypeFinder(c_ast.NodeVisitor):
-    def __init__(self, declname):
-        self.type = None
-
-    def visit_Decl(self, node):
-            self.decl = node
-
-
-class TypeFinder(object):
-    def __init__(self, t):
-        self.type = t
-        self.result = []
-
-    def visit(self, node):
-        if node.__class__.__name__ == self.type.__name__:
-            self.result.append(node)
-        
-        for c in node:
-            self.visit(c)
-    
-
-class TypedIdTransformer(AstPathTransformer):
-    def __init__(self, type_dict):
+class SwitchCasePropertyVisitor(c_ast.NodeVisitor):
+    def __init__(self, state_asmts):
         super().__init__()
-        self.type_dict = type_dict
+        self._sas = state_asmts
+        self.properties = []
 
-    def transform_ID(self, node, path):
-        #print("node[", node.name, "]")
-        #print("pstr[", node.name, "]", path_to_str(path))
-        try:
-            funcdef = next(filter(lambda x:isinstance(x, c_ast.FuncDef), path))
-        except:
-            funcdef = None
-        if funcdef is not None:
-            id_type = None
-            if funcdef.decl.type.args is not None:
-                param_decl = funcdef.decl.type.args.params
-                #print("Param Decl", param_decl)
-                for decl in param_decl:
-                    declfinder = TypeDeclFinder(node.name)
-                    declfinder.visit(decl)
-                    if declfinder.decl is not None:
-                        id_type = self.type_dict.get(declfinder.decl.type.names[0], declfinder.decl.type.names[0])
-                        break
-                if id_type is not None:
-                    #print("pid[", node.name, "]", id_type)
-                    return TypedID(node.name, id_type)
-            
-        return node
-        
-    def transform_StructRef(self, node, path):
-        if isinstance(node.name, c_ast.ID):
-            funcdef = next(filter(lambda x:isinstance(x, c_ast.FuncDef), path))
-            struct_type = None
-            param_decl = funcdef.decl.type.args.params
-            for decl in param_decl:
-                declfinder = TypeDeclFinder(node.name.name)
-                declfinder.visit(decl)
-                if declfinder.decl is not None:
-                    struct_type = self.type_dict.get(declfinder.decl.type.names[0], None)
-                    break
-            name_node = node.name
-            field_node = node.field
-            if struct_type is not None: 
-                name_node = TypedID(node.name.name, struct_type)
-                # find member type
-                declfinder = DeclFinder(field_node.name)
-                declfinder.visit(struct_type)
-                tf = TypeFinder(c_ast.IdentifierType)
-                tf.visit(declfinder.decl.type.type)
-                idtype_str = " ".join(tf.result[0].names)
-                #print("idtype", idtype_str)
-                idtype = self.type_dict.get(idtype_str, idtype_str)
-                field_node = TypedID(node.field.name, idtype)
-            
-            return c_ast.StructRef(name_node, node.type, field_node, node.coord)
-        
-        name_node = self.transform(node.name, path)
-        field_node = self.transform(node.field, path)
-        struct_type = name_node.field.type
-        declfinder = DeclFinder(field_node.name)
-        declfinder.visit(struct_type)
-        tf = TypeFinder(c_ast.IdentifierType)
-        tf.visit(declfinder.decl.type.type)
-        idtype_str = " ".join(tf.result[0].names)
-        idtype = self.type_dict.get(idtype_str, idtype_str)
-        field_node = TypedID(node.field.name, idtype)
-        
-        return c_ast.StructRef(name_node, node.type, field_node, node.coord)
+    def visit_Assignment(self, node):
+        if not(node in self._sas):
+            prop = None
+            if isinstance(node.lvalue, c_ast.StructRef):
+                prop = f"{node.lvalue.children()[0][1].name}->{node.lvalue.children()[1][1].name}<={node.rvalue.name}";
+            else:
+                prop = f"{node.lvalue.name}<={node.rvalue.name}"
+            self.properties.append(prop)
 
-class AstFuncCallInlinerTransformer(object):
-    def __init__(self, func_table):
-        self._method_cache = {}
-        self.func_table = func_table
 
-    def transform(self, node, idtable = None):
-        if idtable is None:
-            idtable = {}
-
-        visitor = self._method_cache.get(node.__class__.__name__, None)
-        if visitor is None:
-            method = 'transform_' + node.__class__.__name__
-            visitor = getattr(self, method, self._transform_generic)
-            self._method_cache[node.__class__.__name__] = visitor
-        
-        return visitor(node, idtable)
-
-    def _transform_Node(self, node, idtable):
-        new_c = []
-        for c_name in node.__slots__[0:-1]:
-            c = getattr(node, c_name)
-            new_c.append(self.transform(c, idtable))
-        node_constructor = node.__class__
-        return node_constructor(*new_c)
-
-    def _transform_generic(self, node, idtable):
-        if isinstance(node, c_ast.Node):
-            return self._transform_Node(node, idtable)
-        elif isinstance(node, list):
-            return [self.transform(x, idtable) for x in node]
-        else:
-            return node
-
-    def transform_FuncCall(self, node, idtable):
-        fcall = node.name.name
-        if fcall in self.func_table:
-            funcdef_args = self.func_table[fcall].decl.type.args.params
-            fcall_args = node.args.exprs
-            if len(fcall_args) != len(funcdef_args):
-                raise Exception("Func Call does not match argument number")
-            # update ID table
-            idtable = idtable.copy()
-            for callarg,defarg in zip(fcall_args, funcdef_args):
-                tdec_finder = TypeFinder(c_ast.TypeDecl)
-                tdec_finder.visit(defarg)
-                if len(tdec_finder.result) == 1:
-                    tdec = tdec_finder.result[0]
-                    paramname = tdec.declname
-                    idtable[paramname] = callarg
-                #print("idtable", idtable)
-            tfnode = self.transform(self.func_table[fcall].body, idtable)
-            return tfnode
-        return node
-    
-    def transform_ID(self, node, idtable):
-        if node.name in idtable:
-            return idtable[node.name]
-        return node
-
-    def transform_TypedID(self, node, idtable):
-        return self.transform_ID(node, idtable)
-    
-    def transform_Assignment(self, node, idtable):
-        op = node.op
-        lvalue = self.transform(node.lvalue, idtable)
-        rvalue = self.transform(node.rvalue, idtable)
-        if op == '-=' or op == '+=' or op == '/=' or op == '*=':
-            operand = op[0]
-            rvalue = c_ast.BinaryOp(operand, lvalue, rvalue)
-            op = '='
-            
-        return c_ast.Assignment(op, lvalue, rvalue, node.coord)
-
-def find_type_of_branch(node):
-    if isinstance(node, c_ast.StructRef):
-        return find_type_of_branch(node.field)
-    elif isinstance(node, TypedID):
-        return node.type
-    else:
-        pass
-    return None
-
-class NuSmvConditionTransformer(AstTransformer):
-    def __init__(self):
+class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor):
+    def __init__(self, case, state_asmts):
         super().__init__()
+        self._case = case
+        self._sas = state_asmts
+        self.properties = []
 
-    def transform_BinaryOp(self, node):
-        op = node.op
-        match op:
-            case '&&':
-                op = '&'
-            case '||':
-                op = '|'
-            case '==':
-                op = '='
-            case _:
-                op = op
-    
-        lhs = node.left
-        rhs = node.right
+    def visit_Case(self, node):
+        label = node.children()[0][1]
+        block = node
+        if label.name == self._case:
+            scpv = SwitchCasePropertyVisitor(self._sas)
+            scpv.visit(block)
+            self.properties += scpv.properties
 
-        lhs_type = find_type_of_branch(lhs)
-        rhs_type = find_type_of_branch(rhs)
-
-        #print("l type:", lhs_type)
-        #print("r type:", rhs_type)
-        #print("l node:", lhs)
-        #print("r node:", rhs)
-        lhs_is_bool = lhs_type == '_Bool'
-        rhs_is_bool = rhs_type == '_Bool'
-        lhs_is_constant = isinstance(lhs, c_ast.Constant)
-        rhs_is_constant = isinstance(rhs, c_ast.Constant)
-        if lhs_is_bool and rhs_is_constant:
-            rhs = c_ast.ID("FALSE" if rhs.value == '0' else "TRUE")
-        elif rhs_is_bool and lhs_is_constant:
-            lhs = c_ast.ID("FALSE" if lhs.value == '0' else "TRUE")
-        
-        lhs = self.transform(lhs)
-        rhs = self.transform(rhs)
-
-        return c_ast.BinaryOp(op, lhs, rhs)
-
-    def transform_ID(self, node):
-        return c_ast.ID(node.name)
-
-    def transform_TypedID(self, node):
-        return c_ast.ID(node.name)
-
-    def transform_StructRef(self, node):
-        def srtf(node):
-            if isinstance(node, c_ast.StructRef):
-                return f"{srtf(node.name)}_{srtf(node.field)}"
-            elif isinstance(node, TypedID) or isinstance(node, c_ast.ID):
-                return node.name
-            return node
-
-        full = srtf(node)
-        return c_ast.ID(full)
-
-    def transform_Cast(self, node):
-        return self.transform(node.expr)
-
-    def transform_Constant(self, node):
-        value = re.sub(r'([a-zA-Z]+)$', '', node.value)
-        return c_ast.Constant(node.type, value)
-
-    def transform_UnaryOp(self, node):
-        return c_ast.UnaryOp(node.op, self.transform(node.expr))
-
-class NuSmvVariableExtractor(c_ast.NodeVisitor):
-    SHORT_TYPE = '−32767..32767'
-    USHORT_TYPE = '0..65535'
-    INT_TYPE = '−32767..32767'
-    UINT_TYPE = '0..65535'
-    TYPE_LUT = {
-        '_Bool':'boolean',
-        'char':'0..255',
-        'signed char':'-127..127',
-        'unsigned char':'0..255',
-        'short':SHORT_TYPE,
-        'short int':SHORT_TYPE,
-        'signed short':SHORT_TYPE,
-        'signed short int':SHORT_TYPE,
-        'unsigned short':USHORT_TYPE,
-        'unsigned short int':USHORT_TYPE,
-        'int':INT_TYPE,
-        'signed':INT_TYPE,
-        'signed int':INT_TYPE,
-        'unsigned':UINT_TYPE,
-        'unsigned int':UINT_TYPE
-    }
-    def __init__(self):
-        self.variables = {}
-    
-    def visit_TypedID(self, node):
-        smvtype = self.TYPE_LUT.get(node.type, None)
-        if smvtype is None:
-            raise Exception(f"Type '{node.type}' is not supported")
-        self.variables[node.name] = smvtype
-
-    def visit_StructRef(self, node):
-        def findfield(node):
-            if isinstance(node, c_ast.StructRef):
-                return findfield(node.field)
-            return node
-        
-        def srtf(node):
-            if isinstance(node, c_ast.StructRef):
-                return f"{srtf(node.name)}_{srtf(node.field)}"
-            elif isinstance(node, TypedID) or isinstance(node, c_ast.ID):
-                return node.name
-            return node
-        field = findfield(node)
-        full = srtf(node)
-        smvtype = self.TYPE_LUT.get(field.type, None)
-        if smvtype is None:
-            raise Exception(f"Type '{field.type}' is not supported")
-        self.variables[full] = smvtype
-        

modelbuilder.py

@@ -1,4 +1,3 @@
-from astvisitors import *
 
 MODEL = """
 ------------------------------------------------------------------------
@@ -6,33 +5,18 @@ MODEL = """
 ------------------------------------------------------------------------
 MODULE {name}
 VAR
-    state : {{ {states} }};
-{variables}
+state : {{ {states} }};
 ASSIGN
     init(state) := {initial};
     next(state) :=
         case
 {transitions}
-            TRUE : state;
         esac;
-{varassigns}
 DEFINE
 {properties}
 """
 
-VARIABLE = "    {n}:{t};"
-
-TRAN = "            (state = {n}) & ({cond}) : {m};"
-CASE = "            {cond} : {value};"
-VARASSIGN = """
-    init({name}) := {initial};
-    next({name}) :=
-        case
-{cases}
-            TRUE : {name};
-        esac;
-"""
-
+TRAN = "            state = {n} : {{{ms}}};"
 PROP = """    -- Property "{prop}"
     {alias} := {logic};
 """
@@ -42,85 +26,64 @@ 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, assigns, ltls=[], name="main"):
+    def __init__(self, states, initial, transitions, properties, ltls=[], name="main"):
         self._name = name
         self._states = states
         self._initial = initial
         self._tran = transitions
-        self._assigns = assigns
+        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):
-        cg = CGenerator()
-        cond_tf = NuSmvConditionTransformer()
-
         # build model
         states_decl = ",".join(self._states)
         transitions = []
-        
-        # find variables in the condition
-        varextract = NuSmvVariableExtractor()
-        
-        for tran in self._tran:
-            cond = cond_tf.transform(tran.condition)
-            if cond is not None:
-                expr = cg.visit(cond)
-            else:
-                expr = 'TRUE'
-            transition = TRAN.format(n=tran.state_from, m=tran.state_to, cond=expr)
-            transitions.append(transition)
-            if tran.condition is not None:
-                varextract.visit(tran.condition)
-        varassigns = []
-        for var,assigns in self._assigns.items():
-            cases = []
-            var_label = var
-            vartype = None
-            for a in assigns:
-                assign_varextract = NuSmvVariableExtractor()
-                #todo convert rvalue to type
-                assign_varextract.visit(a.lvalue)
-                varname, vartype = list(assign_varextract.variables.items())[0]
-                var_label = varname
-                cond = cond_tf.transform(a.condition)
-                cond_expr = cg.visit(cond)
-                varextract.visit(a.condition)
-                varextract.visit(a.lvalue)
-                varextract.visit(a.rvalue)
-                lvalue = var
-                rvalue = cg.visit(cond_tf.transform(a.rvalue))
-                if vartype == 'boolean':
-                    if rvalue == '0':
-                        rvalue = 'FALSE'
-                    elif rvalue == '1':
-                        rvalue = 'TRUE'
-                    else:
-                        pass
-                cases.append(CASE.format(cond=cond_expr, value=rvalue))
-                initial = '0'
-                if vartype == 'boolean':
-                    initial = 'FALSE'
-            varassigns.append(VARASSIGN.format(name=var_label, cases="\n".join(cases),
-                                               initial=initial))
-            #print(cases)
 
-        variables = []
-        for v,t in varextract.variables.items():
-            variables.append(VARIABLE.format(n=v, t=t))
-        
+        for n,ms in self._tran.items():
+            transition = TRAN.format(n=n, ms=",".join(ms))
+            transitions.append(transition)
+
         properties = []
-        #for alias,(states,prop) in self._props.items():
-        #    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)
+        for prop,states 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)
 
         out = MODEL.format(name=self._name,
                             states=states_decl,
-                            variables="\n".join(variables),
                             initial=self._initial,
                             transitions="\n".join(transitions),
-                            varassigns="\n".join(varassigns),
                             properties="\n".join(properties))
 
         # add LTL formulas

utils.py

@@ -1,33 +1,5 @@
 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 remove_prefix(s, prefix):
-    return s[len(prefix):] if s.startswith(prefix) else s
-
 def find_longest_path(paths):
     ms = 0
     mp = None