symdivine ltl error

[nisrine]

Hi, I got the same error as an input for all the models that I've tried when trying to verify LTL property.
which is:

Unknown token!
terminate called after throwing an instance of 'std::runtime_error'
what(): ERROR: syntax error, unexpected $end
Aborted (core dumped)

And for the reachability for one of my models I got this output

symdivine: /home/nisrine/SymDIVINE-master/src/llvmsym/memorylayout.h:133: void llvm_sym::MemoryLayout::setMultival(llvm_sym::MemoryLayout::VariableId, bool): Assertion `variable.segmentId < variablesFlags.size()' failed.
Aborted (core dumped)

Any help please,
thank you.

[yaqwsx]

Hi,
the first error marks you have invalid syntax in your LTL fromula. Could you send it?

The second error is related to #6, are you using pointers in your program?

[nisrine]

Hi, thanks for your quick response. My LTL formula is :
(G((updateSM = PENDING) => F (updateSM == PROCESS)))
For the second one no I'm not using pointers in my program

[yaqwsx]

Atomic proposition has to be enclosed in [] and has to refer to global variables (global variables are named seg1_off{x}, where {x} is their index in bitcode file). So your formula should look like this: (G([seg1_off0 = 0(32)] => F [seg1_off1 = 1(32)])).

[nisrine]

Hi, I still get the same error even after the modification of the property.
I've also tried with a very basic C program, and I have the same error. also in the examples in the zip attached
symDivine.tar.gz

[yaqwsx]

There are the same examples with their properties written in property.ltl file.
ltl.zip

[nisrine]

Please check if I'm using the correct model in this example

:/SymDIVINE-master$ bin/symdivine reachability ../Downloads/ltl/afp-succeed/model_op.ll
Safe.
nisrine@nisrine:/SymDIVINE-master$ bin/symdivine ltl ../Downloads/ltl/afp-succeed/property.ltl ../Downloads/ltl/afp-succeed/model_op.ll
Unknown token!
terminate called after throwing an instance of 'std::runtime_error'
what(): ERROR: syntax error, unexpected $end
Aborted (core dumped)

[yaqwsx]

bin/symdivine ltl  `cat ../Downloads/ltl/afp-succeed/property.ltl` ../Downloads/ltl/afp-succeed/model_op.ll

[nisrine]

As an ouput for the command I got :

Unexpected argument: ltl, cat, ../Downloads/ltl/afp-succeed/property.ltl, ../Downloads/ltl/afp-succeed/model_op.ll
SymDIVINE.

Why you added cat ?

[yaqwsx]

GitHub escaped quotes - I updated the comment.

[nisrine]

First thanks a lot for your help, but still not working.
For the example I got

:~/SymDIVINE-master$ bin/symdivine ltl \cat ../Downloads/ltl/afp-succeed/property.ltl../Downloads/ltl/afp-succeed/model_op.ll
bash: ../Downloads/ltl/afp-succeed/model_op.ll: Permission denied
../Downloads/ltl/afp-succeed/property.ltl: ../Downloads/ltl/afp-succeed/property.ltl:1:2: error: expected integer
!(F([seg1_off0 != 0(32)]))
^

I also tried on my program and got:

:~/SymDIVINE-master$ bin/symdivine ltl \cat prop.ltlmain.ll
main.ll: command not found
prop.ltl: prop.ltl:1:1: error: expected top-level entity
(G([updateSM = 601] => F [updateSM = 602]))
^

What do you think it is related to?

Thanks again