From 92c32b6807c4bcdc43186d007a07f0b921816c44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominic=20H=C3=B6glinger?= Date: Sun, 20 Nov 2022 22:20:15 +0100 Subject: [PATCH] added sucky graphviz export of kripke --- analyze.py | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/analyze.py b/analyze.py index a64f821..00483a7 100644 --- a/analyze.py +++ b/analyze.py @@ -1,9 +1,10 @@ from __future__ import print_function import argparse import sys -from modelbuilder import * - from pycparser import parse_file, c_ast +import graphviz as gv + +from modelbuilder import * func_table = {} enum_table = {} @@ -181,6 +182,7 @@ if __name__ == "__main__": 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') + argparser.add_argument('--dot', help='output dot file') args = argparser.parse_args() ast = parse_file(args.filename, use_cpp=False) @@ -275,3 +277,21 @@ if __name__ == "__main__": 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)