About LTL checking

[germa...@gmail.com]

Hi everybody

I have a big LTL expression encoding a temporal ER model and I need to check it for satisfiability.

I cannot find any suitable LTL file example in order to use ProB properly. Please, could anybody help me?

Thanks a lot!

[Michael Leuschel]

Hi,

have you looked at the manual page:
https://www3.hhu.de/stups/prob/index.php/LTL_Model_Checking

Below is a small example using probcli, where LTL formulas were stored in a file:

probcli SimpleWithConstants.mch -ltlfile SimpleWith.ltl
% Runtime for SOLUTION for SETUP_CONSTANTS: 30 ms (walltime: 31 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
LTL Model checking assertions
Checking formula Globally an atomic proposition:
LTL model checking: memory usage approx. 1796 KiB, 16 atoms and 12 transitions generated
LTL model checking: total time 11ms, 4 callbacks needed 10ms, netto 0ms.
LTL model checking: memory usage approx. 1282 KiB, 1 atoms and 0 transitions generated
LTL model checking: total time 0ms, 1 callbacks needed 0ms, netto 0ms.
LTL model checking: memory usage approx. 1924 KiB, 20 atoms and 17 transitions generated
LTL model checking: total time 0ms, 4 callbacks needed 0ms, netto 0ms.
Checking formula A transition proposition:
Checking formula Another transition proposition:
All LTL formulas checked.

Greetings,
Michael

> --
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/0b1f7ca7-5584-4cd4-a84c-e81962028554%40googlegroups.com.