yanntm
commented
7 years ago Well, the bug seems not to exist in 3.0, so that's good. Attached the 3.0 compliant files gal.zip
Good also, I managed to upgrade my API calls to use 3.0 now.
Closed yanntm closed 7 years ago
Hi
I'm running into a segfault with a pretty simple model gal.zip
I'm using : pins2lts-seq gal.so -p -when -i "EratosthenesPT010ReachabilityFireability0==true"
A couple of traces bleow, it only crashes with -por. The model is Eratosthenes-010 from the MCC.
ythierry@localhost ITS-Tools-pnmcc (master)]$ lts_install_dir/bin/pins2lts-seq INPUTS/Eratosthenes-PT-010/gal.so -p --when -i "EratosthenesPT010ReachabilityFireability0==true" pins2lts-seq, 0.000: Registering PINS so language module pins2lts-seq, 0.000: Loading model from INPUTS/Eratosthenes-PT-010/gal.so pins2lts-seq, 0.000: library has no initializer pins2lts-seq, 0.000: loading model GAL pins2lts-seq, 0.000: completed loading model GAL pins2lts-seq, 0.000: Initializing POR dependencies: labels 13, guards 8 pins2lts-seq, 0.000: Expression is: (EratosthenesPT010ReachabilityFireability0 == true ) pins2lts-seq, 0.000: Forcing the use of a cycle proviso. For best results use --proviso=color. pins2lts-seq, 0.000: There are 13 state labels and 1 edge labels pins2lts-seq, 0.000: State length is 5, there are 8 groups pins2lts-seq, 0.000: Running dfs search strategy pins2lts-seq, 0.000: Using a tree for state storage pins2lts-seq, 0.000: Visible groups: 0 / 8, labels: 1 / 13 pins2lts-seq, 0.000: POR cycle proviso: stack segmentation fault
Please send information on how to reproduce this problem to: ltsmin-support@lists.utwente.nl along with all output preceding this message. In addition, include the following information: Package: ltsmin 2.1 Stack trace: 0: lts_install_dir/bin/pins2lts-seq(HREprintStack+0x18) [0x4311a8] 1: lts_install_dir/bin/pins2lts-seq() [0x431226] 2: /lib64/libpthread.so.0(+0x10bb0) [0x7f5512acebb0] 3: lts_install_dir/bin/pins2lts-seq() [0x44bed8] 4: lts_install_dir/bin/pins2lts-seq(qsortr+0x20b) [0x45916b] 5: lts_install_dir/bin/pins2lts-seq() [0x4505fb] 6: lts_install_dir/bin/pins2lts-seq() [0x41cb25] 7: lts_install_dir/bin/pins2lts-seq() [0x41c33a] 8: lts_install_dir/bin/pins2lts-seq() [0x41c2e4] 9: lts_install_dir/bin/pins2lts-seq(main+0x81a) [0x41b47a] 10: /lib64/libc.so.6(__libc_start_main+0xf0) [0x7f551242b600] 11: lts_install_dir/bin/pins2lts-seq() [0x41c13d]
No crash without POR :
[ythierry@localhost ITS-Tools-pnmcc (master)]$ lts_install_dir/bin/pins2lts-seq INPUTS/Eratosthenes-PT-010/gal.so --when -i "EratosthenesPT010ReachabilityFireability0==true" pins2lts-seq, 0.000: Registering PINS so language module pins2lts-seq, 0.000: Loading model from INPUTS/Eratosthenes-PT-010/gal.so pins2lts-seq, 0.000: library has no initializer pins2lts-seq, 0.000: loading model GAL pins2lts-seq, 0.000: completed loading model GAL pins2lts-seq, 0.000: Expression is: (EratosthenesPT010ReachabilityFireability0 == true ) pins2lts-seq, 0.000: There are 13 state labels and 1 edge labels pins2lts-seq, 0.000: State length is 5, there are 8 groups pins2lts-seq, 0.000: Running dfs search strategy pins2lts-seq, 0.000: Using a tree for state storage pins2lts-seq, 0.000:
pins2lts-seq, 0.000: Invariant violation (EratosthenesPT010ReachabilityFireability0==true) found at depth 4! pins2lts-seq, 0.000:
pins2lts-seq, 0.000: exiting now
Under gdb (but no symbols sorry)
Program received signal SIGSEGV, Segmentation fault. 0x000000000044bed8 in score_cmp () (gdb) bt
0 0x000000000044bed8 in score_cmp ()
1 0x000000000045916b in qsortr ()
2 0x00000000004505fb in por_beam_search_all ()
3 0x000000000041cb25 in dfs_state_next_all ()
4 0x000000000041c33a in gsea_foreach_open_cb ()
5 0x000000000041c2e4 in gsea_foreach_open ()
6 0x000000000041b47a in main ()