utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

opaal2lts-mc: undefined symbol lattice_clone #176

Open jacopol opened 4 years ago

jacopol commented 4 years ago

A number of testcases in opaal/tests fail because the symbol "lattice_clone" is not found.

Example: opaal2lts-mc channel_array.so opaal2lts-mc( 0/ 4), error : dynamically loading from `channel_array.so': /mnt/c/Users/au616260/Opaal/channel_array.so: undefined symbol: lattice_clone

Analysis: it seems that channel_array.cpp doesn't include any DBM-related code. So this is probably an issue in opaal's gensuccgen.py. In particular, the definition extern "C" dbm::fed_t lattice_clone (const dbm::fed_t fed) is missing in channel_array.cpp. (it is present in other examples)

I'm using this script to reproduce this behavior:

BASEDIR=/home/jaco/opaal-ltsmin EXAMPLE=$BASEDIR/opaal/tests/gensuccgen/channel_array.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 --state=table --threads=1 $FILE.so