-ltlfile

[Franco Mazzanti]

I  cannot find a way to call probcli with a file containing a list of formulas.

I always get the message:

> ! An error occurred (source: ltl) !
> ! Error while parsing the LTL formula file
> An error occurred while parsing the LTL file.

The formulas are correct as when used inside the GUI they are correctly veririfed.

Is it possible to see a valid  example of ltlfile ?

Or maybe there is some bug in the ltlfile parsing?

(Prob 1.9,  MacOS 10.13.6)

Best regards

Franco Mazzanti

franco....@isti.cnr.it

[Dobrikov]

Hi Franco,

each LTL formula in the file must be preceded by [Name], where Name is a random name given by the user. In the attachment of this email you can find an example of an LTL-file with multiple formulae for classical B models.

You can also read the following tutorial on the ProB site: https://www3.hhu.de/stups/prob/index.php/LTL_Model_Checking

Best Regards

Ivaylo Dobrikov

[Franco Mazzanti]

Many thans!!

I knew expected logical structure as hinted in the documentation  on LTL_Model_Checking.

My mistake was that of not going to a new line when writing the formula.

Thans again

Franco