K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Dear Samira,

what do you mean by "the performance of this model"? If you refer the time used by the (Maude) model-checker algorithm, then krun does not supply such information. This can be obtained by running directly Maude system with a command like the following one:

maude cink-kompiled/main.maude .k/krun/maude_in.maude

The example cink/ltlmc explains the main idea how to use the Maude LTL model checker together with K.
You must add the following ingredients to your definition: import the modules  LTL-HOOKS and MODEL-CHECKER-HOOKS, define the syntax of the atomic propositions and their semantics. In order to define the model to be checked, you must tag as transitions the K rules that define the transitions in your model.
The tagging can be done in two ways: using direct the tag "transition" in the definition of the rule or (more flexible) to use the "--transition" option of the kompile tool.
Then you must use the execution command krun together with the option "--ltlmc", giving as argument for this option the LTL formula (as string or stored into a file).

The syntax for the LTL operators is that from Maude, but where the suffix "Ltl" is added (see cink/ltlmc/programs/form-dekker.cink for an example).

That is all.

Dorel

On 8/5/13 1:27 PM, samira kherfellah wrote:

Hi All,

I have a question about the model checker of cink example, how we can have the performance of this model?

how to use LTL model checker to check properties in K?

Samira

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user