Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

opaal2lts-mc/ltsmin-convert: string doesn't start with double quote #178

Open
jacopol opened this issue Nov 14, 2019 · 0 comments
Open

opaal2lts-mc/ltsmin-convert: string doesn't start with double quote #178

jacopol opened this issue Nov 14, 2019 · 0 comments

Comments

@jacopol
Copy link
Contributor

jacopol commented Nov 14, 2019

On one example generating a gcf from an opaal-specification and transforming it to an fsm file (for human readability) fails:

opaal2lts-mc train-gate.so train-gate.gcf
ltsmin-convert --rdwr train-gate.gcf train-gate.fsm

Explored 726857 states 1055640 transitions, fanout: 1.452
ltsmin-convert, ** error **: string does not start with double quote

The root cause might be in Opaal's gensuccgen.py, since that script gives warnings (however, it continues to produce some result):
WARNING:pyuppaal.analyzer:Unknown expression: Node(Equal, (Node(Number, [], 0), Node(FunctionCall, [Node(Identifier, ['Gate_front'], None)], [])), [])

Use the following script to reproduce:

BASEDIR=/home/jaco/opaal-ltsmin
EXAMPLE=$BASEDIR/opaal/tests/ltl_tests/train-gate.xml
FILE=basename $EXAMPLE .xml

export PYTHONPATH=$BASEDIR/pyuppaal:$BASEDIR/opaal:$BASEDIR/usr/lib/python2.7/site-packages/
export LTSMIN_MEM_SIZE=68719476736

python $BASEDIR/opaal/opaal/model_parsers/pyuppaal/gensuccgen.py $EXAMPLE $FILE.cpp
g++ -g -shared -O2 -fPIC -I$BASEDIR/usr/uppaal/include/ -L$BASEDIR/usr/uppaal/lib/ -o $FILE.so $FILE.cpp -ludbm
opaal2lts-mc --strategy=bfs --state=table -u1 --threads=1 $FILE.so $FILE.gcf
ltsmin-convert --rdwr $FILE.gcf $FILE.fsm

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant