utwente-fmt / ltsmin

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

spins -S not compiling properly #136

Closed jacopol closed 7 years ago

jacopol commented 7 years ago

Below, spins -S generates code that refers to matrices that have not been generated

Command line: spins -S garp/garp-a/garp.pml SpinS Promela Compiler - version 1.1 (3-Feb-2015)

...

Written C code to /home/vdpol/PromelaDemo/garp.pml.spins.c garp.pml.spins.c: In function ‘disabled_by’: garp.pml.spins.c:7601:12: error: ‘dm_must_disable’ undeclared (first use in this function) return dm_must_disable[guard][o]; ^ garp.pml.spins.c:7601:12: note: each undeclared identifier is reported only once for each function it appears in garp.pml.spins.c: In function ‘nes_has’: garp.pml.spins.c:7605:12: error: ‘nes_dm’ undeclared (first use in this function) return nes_dm[guard][o]; ^ garp.pml.spins.c: In function ‘nds_has’: garp.pml.spins.c:7609:12: error: ‘nds_dm’ undeclared (first use in this function) return nds_dm[guard][o]; ^ garp.pml.spins.c: In function ‘not_coenabled’: garp.pml.spins.c:7613:13: error: ‘co_dm’ undeclared (first use in this function) return !co_dm[guard][o]; ^ garp.pml.spins.c: In function ‘spins_create_matrices’: garp.pml.spins.c:7670:18: error: ‘dna_dm’ undeclared (first use in this function) if (!dna_dm[i][j]) { ^ garp.pml.spins.c: In function ‘spins_create_matrix_visitor2’: garp.pml.spins.c:8000:50: error: ‘nes_dm’ undeclared (first use in this function) case 'e': return spins_create_matrix_visitor(nes_dm[0], l, t, invert, c, check); ^ garp.pml.spins.c:8001:50: error: ‘nds_dm’ undeclared (first use in this function) case 'd': return spins_create_matrix_visitor(nds_dm[0], l, t, invert, c, check); ^ garp.pml.spins.c:8002:50: error: ‘commutes_dm’ undeclared (first use in this function) case 'u': return spins_create_matrix_visitor(commutes_dm[0], t, t, invert, c, check); ^ garp.pml.spins.c:8003:50: error: ‘dna_dm’ undeclared (first use in this function) case 'a': return spins_create_matrix_visitor(dna_dm[0], t, t, invert, c, check); ^ garp.pml.spins.c:8006:50: error: ‘co_dm’ undeclared (first use in this function) case 'c': return spins_create_matrix_visitor(co_dm[0], l, l, invert, c, check); ^ garp.pml.spins.c:8008:50: error: ‘dm_must_disable’ undeclared (first use in this function) case 'm': return spins_create_matrix_visitor(dm_must_disable[0], l, t, invert, c, check); ^ garp.pml.spins.c: At top level: cc1: warning: unrecognized command line option "-Wno-unknown-warning-option" [enabled by default] cc1: warning: unrecognized command line option "-Wno-initializer-overrides" [enabled by default] cc1: warning: unrecognized command line option "-Wno-parentheses-equality" [enabled by default] Compilation of garp.pml.spins.c failed

alaarman commented 7 years ago

Fixed in 39715314c3634d3d591d71e1965746825eaba991