Krun --ltlmc

[smaaliSahar]

Hello, I want to use K model checking tool, but i keep getting this message every time I krun an example:

[Error] Critical: Backend java does not support ltl model checking. Supported backends are: []

what should i do?? Thanks for your help.

[dwightguth]

If you want to use model checking, currently you will need to back up your definition to K 3.5. K 3.6 does not yet support model checking; we intend to address this at some point before the release of K 4.0, however, that work is not yet complete.

[omarzd]

Can you please point me to documentation on how to use model checking? I don't even know the syntax for defining a property.

[smaaliSahar]

You may find examples in cink-semantics: https://github.com/kframework/cink-semantics

[dwightguth]

@traiansf It would be good if we could get to the point with your plugin where this can be used as a replacement for the Maude LTLMC. What is the status of that work?

[traiansf]

With the caveat that it's awfully slow and it uses a lot of memory, w.r.t. functionality it's getting pretty close. However, in order to be able to integrate it, we would need first do design a language/convention for how state predicates are to be specified and evaluated.

What I have now it's rather ad-hoc and verbose.

[dwightguth]

How difficult would it be to adapt your algorithm so that it used matching logic patterns as state predicates?

[traiansf]

Matching logic patterns should be quite fine. However, I see a couple things which need clarification:

• The patterns should be named, to allow repeating them inside a formula
• should/could the patterns, i.e., atomic predicates, be parameterized? It is not standard LTL practice, but usage of parameterized LTL predicates in Maude's LTL model checker proved to be nice.
• the LTL parser we currently use (extracted from NASA JPF source code) only accepts non-parameterized atomic predicates; if we want to use atomic predicates with any kind of structure, including parameters, we first need to write our own parser for that.

[grosu]

The patterns should be named, to allow repeating them inside a formula

This is trivial, isn't it? E.g.:

syntax Sort ::= name(P1,P2,P3)
rule name(P1,P2,P3) => pattern involving parameters P1, P2 and P3  [macro]

For example, suppose that you want a pattern where program variable x points to a list in the heap. Then we can have

syntax Bag ::= mylist(Id,List{Int})
rule mylist(X,A) => <env>... X |-> ?L ...</env>  <heap>... list(?L,A) ...</heap>

should/could the patterns, i.e., atomic predicates, be parameterized? It is not standard LTL practice, but usage of parameterized LTL predicates in Maude's LTL model checker proved to be nice.

As shown above, they can, can't they?

LTL parser

That should be really easy with the new parser.

[grosu]

BTW, I think we should all look into the work of Javier Esparza, who came up with some very powerful techniques for push-down system model checking: https://www7.in.tum.de/~esparza/. I talked to him once and it looked like K is a perfect setting for such techniques, because it is stack-based. We should be able to identify some K definitions for which we can use his fast algorithms.

[dlucanu]

I guess that "pattern" was used for a ML formula, e.g. \pi /\ \phi, so the codition part \phi must be mentioned as well. Moreover, the basic pattern \pi must be concretized and I do not know if this happens for the case of macros.

Dorel

On 29/04/15 16:33, Grigore Rosu wrote:

The patterns should be named, to allow repeating them inside a formula

This is trivial, isn't it? E.g.:

syntax Sort ::= name(P1,P2,P3) rule name(P1,P2,P3) => pattern involving parameters P1, P2 and P3 [macro]

For example, suppose that you want a pattern where program variable |x| points to a list in the heap. Then we can have

syntax Bag ::= mylist(Id,List{Int}) rule mylist(X,A) => ... X	-> ?L ... ... list(?L,A) ...

should/could the patterns, i.e., atomic predicates, be
parameterized? It is not standard LTL practice, but usage of
parameterized LTL predicates in Maude's LTL model checker proved
to be nice.

As shown above, they can, can't they?

LTL parser

That should be really easy with the new parser.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1285#issuecomment-97427598.

[dlucanu]

We used a modified version of Stefan Schwoon's algorithm, one of his PhD students.

Dorel

On 29/04/15 16:46, Grigore Rosu wrote:

BTW, I think we should all look into the work of Javier Esparza, who came up with some very powerful techniques for push-down system model checking: https://www7.in.tum.de/~esparza/ https://www7.in.tum.de/%7Eesparza/. I talked to him once and it looked like K is a perfect setting for such techniques, because it is stack-based. We should be able to identify some K definitions for which we can use his fast algorithms.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1285#issuecomment-97430305.

[traiansf]

I personally don't like this rule-based approach because a predicate should be kind of boolean sort, not of Bag sort and might additionally have constraints over the variables matched in the configuration pattern.

When discussing with @dlucanu about this, we were thinking that K should allow users to specify and name (parameterized) ML formulas. This could be useful in other instances, such as maybe symplifying RL formulas. It could have a syntax like:

pattern a(X:Id) ::= <env>... X |-> N:Int ...</env> <store>... N |-> Z:Int ...</store> requires Z =/=Int 0

(maybe we could use something else instead requires, since here there is no left-right direction as for rules)

similarly your pattern could be written as

`pattern mylist(X:Id,A:List{Int}) ::= ... X |-> ?L ...

... list(?L,A) ...` then one could write ltl formulas where patterns are atoms. Parsing them is probably not a problem, but having parameterized formulas might make it harder to use off-the-shelf ltl-to-promela conersion tools.

[dwightguth]

I think I would propose that to start with, we should have only unparametrized formulas, and that we parse them as rules, like Grigore says, in a special module that is passed as part of the ltl invocation. This simplifies the implementation while giving us everything that we need at a basic level.

Traian, how much work would it be for you to write code that takes the string passed via ltl and parses it using the same parser used for proof specifications, then extracts the rhs and the side condition and renders it into a form that the ltl model checker can use?

[traiansf]

I think I would propose that to start with, we should have only unparametrized formulas, and that we parse them as rules, like Grigore says, in a special module that is passed as part of the ltl invocation. This simplifies the implementation while giving us everything that we need at a basic level.

I guess I could make a concession (for now) to what you and Grigore suggest. If we are only to handle atomic predicates, then we could have a predefined partial function

Bag ::= ltlPattern(String)

and use it to define the patterns with rules like you said.

rule ltlPattern("criticalA") => <a> critical </a>
rule ltlPattern("waitB") => <b> wait </b>

Note, however, that these rules need to be given special attention during compilation, in the sense that the right-hand-side needs to be context-transformed up to the top level. But perhaps this can be done in krun, though.

Traian, how much work would it be for you to write code that takes the string passed via ltl and parses it using the same parser used for proof specifications, then extracts the rhs and the side condition and renders it into a form that the ltl model checker can use?

I'm not sure what you mean here. Remember that I don't have direct access to the rewrite engine, so everything I do is currently done through the krun interface.

I see two options:

1. Krun exports a satisfiesPattern method which given a state and the name of an ltlPattern, it checks whether the state matches the rhs of the corresponding tltPattern rule and the condition holds
2. Kompile encodes these rules into satisfaction rules like the ones I'm now writing by hand, and adds them to the definition rules and then what I'm using now would work.

I would actually prefer something like option 1, and I think it would be something useful to other projects, too.

[dwightguth]

Okay, I see. What you want to do then is the same thing that is done if --pattern is specified but not --search, namely, do a search on zero steps with the specified pattern. So bascially, you will take the rhs of the rule and the requires clause, and construct a search pattern from it, which will be passed to the search() method of the KRun interface. If it has results, then the pattern matches, otherwise, the pattern does not match.

On Wed, Apr 29, 2015 at 2:03 PM, Traian Florin Șerbănuță < notifications@github.com> wrote:

I think I would propose that to start with, we should have only unparametrized formulas, and that we parse them as rules, like Grigore says, in a special module that is passed as part of the ltl invocation. This simplifies the implementation while giving us everything that we need at a basic level.

I guess I could make a concession (for now) to what you and Grigore suggest. If we are only to handle atomic predicates, then we could have a predefined partial function

Bag ::= ltlPattern(String)

and use it to define the patterns with rules like you said.

rule ltlPattern("criticalA") => <a> critical </a>
rule ltlPattern("waitB") => <b> wait </b>

Note, however, that these rules need to be given special attention during compilation, in the sense that the right-hand-side needs to be context-transformed up to the top level. But perhaps this can be done in krun, though.

Traian, how much work would it be for you to write code that takes the

string passed via ltl and parses it using the same parser used for proof specifications, then extracts the rhs and the side condition and renders it into a form that the ltl model checker can use?

I'm not sure what you mean here. Remember that I don't have direct access to the rewrite engine, so everything I do is currently done through the krun interface.

I see two options:

1. Krun exports a satisfiesPattern method which given a state and the name of an ltlPattern, it checks whether the state matches the rhs of the corresponding tltPattern rule and the condition holds
2. Kompile encodes these rules into satisfaction rules like the ones I'm now writing by hand, and adds them to the definition rules and then what I'm using now would work.

I would actually prefer something like option 1, and I think it would be something useful to other projects, too.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1285#issuecomment-97543516.

[dlucanu]

The idea with search on zero steps for a ML pattern is nice and I think very useful.