dominic/kripkomat
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

added sucky graphviz export of kripke

Browse Source
This commit is contained in:
Dominic Höglinger 2022-11-20 22:20:15 +01:00
parent acb433c8c4
commit 92c32b6807
1 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
analyze.py
View File

@ -1,9 +1,10 @@
from __future__ import print_function from __future__ import print_function
import argparse import argparse
import sys import sys
from modelbuilder import *
from pycparser import parse_file, c_ast from pycparser import parse_file, c_ast
import graphviz as gv
from modelbuilder import *
func_table = {} func_table = {}
enum_table = {} enum_table = {}
@ -181,6 +182,7 @@ if __name__ == "__main__":
argparser.add_argument('--initial', help='initial state') argparser.add_argument('--initial', help='initial state')
argparser.add_argument('--ltlfile', help='file containing LTL formulae') argparser.add_argument('--ltlfile', help='file containing LTL formulae')
argparser.add_argument('-o', '--output', dest='output', help='output NuSMV file') argparser.add_argument('-o', '--output', dest='output', help='output NuSMV file')
argparser.add_argument('--dot', help='output dot file')
args = argparser.parse_args() args = argparser.parse_args()
ast = parse_file(args.filename, use_cpp=False) ast = parse_file(args.filename, use_cpp=False)
@ -275,3 +277,21 @@ if __name__ == "__main__":
print("-------------------") print("-------------------")
print(nusmv) 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)