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)], [])), [])
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 .xmlexport 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