LTL does not work anymore

Description

Prolog throws exceptions when trying to check a LTL Formula, for instance G {done=1}

I have tried the released version of the cli as well as the nightly build. Both versions throw (different) exceptions.

Environment

None

Attachments

4

Gliffy Diagrams

Activity

Show:

Jens Bendisposto June 17, 2014 at 8:55 AM

Released fixed version

Jens Bendisposto June 17, 2014 at 4:48 AM

Fixed in nightly.

Michael Leuschel June 16, 2014 at 12:19 PM

The predicate pp_formulas was not exported in ltl_tools.pl.
Have just fixed this.

Daniel: it is maybe a bit unfortunate that in order to see the trace the user has to click on the graphical counterexample.
The "uninitialised" trace in the History view is a bit misleading, I think.
(See screenshot.)

Michael Leuschel June 16, 2014 at 12:10 PM

Using the latest ProB Tcl/Tk Version all works well:
ERED

% writing_formula_to_file(B,ltl_formulas.txt)
% calling_ltl_parser(/usr/bin/java,[-cp,/Users/leuschel/git_root/prob_prolog/lib/probcliparser.jar,de.prob.cliparser.LtlConsoleParser,-ltl,-lang,B,/var/folders/j4/cxrp94290tdg3mgpvg8yjfdc0000gn/T/ltl_formulas.txt])
Predicate call: ltl_model_check('G ({done = 1})',10000,init,Res)
% parsing_ltl_formula
% writing_formula_to_file(B,ltl_formulas.txt)
% calling_ltl_parser(/usr/bin/java,[-cp,/Users/leuschel/git_root/prob_prolog/lib/probcliparser.jar,de.prob.cliparser.LtlConsoleParser,-ltl,-lang,B,/var/folders/j4/cxrp94290tdg3mgpvg8yjfdc0000gn/T/ltl_formulas.txt])
LTL model checking: found counter-example (lasso-form): intro length = 0, path in SCC of length = 2
LTL model checking: memory usage approx. 1668 KiB, 4 atoms and 4 transitions generated
LTL model checking: total time 0ms, 2 callbacks needed 0ms, netto 0ms.
% initialising_ltlc
starting_model_checking

Fixed

Details

Assignee

Reporter

Priority

More fields

Created June 16, 2014 at 10:02 AM
Updated June 17, 2014 at 8:55 AM
Resolved June 17, 2014 at 4:48 AM