K-user mailing list

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

For the moment, K Tool uses in the back-end the Maude LTL model-checker.
Therefore its performances on model-checking are inherited from Maude.
You may call directly Maude in order to get information about time and number of rewrites, the usual information Maude supplies:

$ maude lang-kompiled/main.maude .k/krun/maude_in.maude

However, the efficiency of the algorithm strogly depend on the size of the generated transition system.
You may increase or decrease the size of the transition system by adding or removing the tag "transition" for rules.
More flexible is the use of the option "-transition" of the kompile tool; with it you may generate different transition systems without changing the definitions.
For that you must assign appropriate labels to rules, similar to "kripke" in cink/ltlmc.

Dorel


 

On 5/1/13 2:48 PM, samira kherfellah wrote:

Hi All,

In k, to represent the model_checking, LTL formulas are used. (two modules,
one for the syntax and an another for the semantics ).

But how to evaluate performance of model_checking  in K?

For example, how can we have the execution time, the occupation of the
memory?

Sincerely,
Samira

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