Skip to main content

Notice: this Wiki will be going read only early in 2024 and edits will no longer be possible. Please see: https://gitlab.eclipse.org/eclipsefdn/helpdesk/-/wikis/Wiki-shutdown-plan for the plan.

Jump to: navigation, search

Difference between revisions of "Henshin/State Space Tools"

m (Move link to subpage and add category Modeling)
(60 intermediate revisions by 3 users not shown)
Line 1: Line 1:
To verify correctness of transformations, Henshin provides a tool for  
+
To verify the correctness of transformations, Henshin provides tools for  
analysing the state spaces of in-place model transformation. To some extent
+
generating and analyzing the state spaces of in-place model transformation.  
this can be compared to a debugger: starting from some initial state, the  
+
Starting from some initial state, the transformation is executed in a  
transformation is executed in a stepwise fashion and can be thus analysed,  
+
stepwise fashion and can be, thus, analyzed, e.g. to make sure that all
e.g. to make sure that intermediate states are correct. However, state space
+
intermediate states are correct fulfill some invariants.  
analysis is much more powerful than debugging, because instead of inspecting
+
one particular execution path, the complete state space incuding all possible
+
paths is generated. It goes without saying that the state space should be finite
+
for this to work.
+
  
Once the state space is generated for a particulare transformation and start
+
The state space tools in Henshin currently support the following features:
state, it can be analysed in Henshin using a various number of (external)  
+
[[Image:Statespace-explorer-phil-win32.png|320px|thumb|right|Henshin State Space Explorer]]
validation tools. Currently supported are:
+
* Efficient (multi-threaded), resumable generation of explicit state spaces
 +
* State-based abstractions:
 +
** Ignoring link orders (graph isomorphy)
 +
** Ignoring certain attributes
 +
** Optional object IDs
 +
* Interactive state space generation and visualization
 +
* Extensible validation/verification framework:
 +
** Structural state invariant checking using OCL
 +
** Qualitative model checking using [http://www.inrialpes.fr/vasy/cadp CADP] and [http://www.mcrl2.org mCRL2]
 +
** Probabilistic model checking using [http://www.prismmodelchecker.org PRISM]
 +
* Extensible export functionality:
 +
** TikZ (*.tex)
 +
** CADP (*.aut)
 +
** PRISM (*.sm, *.nm, *.tra etc.)
  
* (Structural) state invariant checking with OCL
+
All these functionalities are integrated in a graphical state space explorer, shown on the right. They can be also invoked from the context menu for state space files or
* Qualitative model checking using [http://www.inrialpes.fr/vasy/cadp CADP] and [http://www.mcrl2.org mCRL2]
+
programmatically. For model checking, the state space explorer provides a uniform front-end to the above mentioned analysis tools.  
* Probabilistic model checking using [http://www.prismmodelchecker.org PRISM].
+
  
Henshin's state space explorer allows you to generate and visualize state space
 
and moreover provides a front-end to the above mentioned analysis tools.
 
  
[[Image:statespace-explorer-phil.png|300px|x]]
+
__TOC__
  
  
== Generating the State Space ==
+
= State space generation =
  
As a running example we consider the academic example of dining philosophers.
+
In this section, we explain how to generate a state space for a Henshin transformation.
To make it more interesting we include a rule for a dynamic reconfiguration, i.e.
+
to allow to add a philosopher to the table during the execution. The rules
+
are depicted below. We have two rule ''left'' and ''right'' for picking up
+
forks, a rule ''release'' for putting them back on the table, and finally a rule
+
''create'' for squeezing in a new philosopher. We include negative application
+
conditions to make sure that we cannot add arbitrarily many philosophers.
+
This is important to ensure that the state space is finite. Here we chose
+
an upper limit of at most 5 philosophers.
+
We should also point out again that we can model both the
+
execution and the reconfiguration using transformation rules in Henshin.
+
  
[[Image:statespace-phil-left.png|200x100px|x]] [[Image:statespace-phil-release.png|200x100px|x]] [[Image:statespace-phil-create.png|200x100px|x]]
+
== Transformation rules and initial state ==
  
Now that we have defined our transformation rules, we need to create an initial
+
As a running example we consider the academic example of dining philosophers documented [http://www.eclipse.org/modeling/emft/henshin/examples.php?example=diningphils here]. To make it more interesting we include a rule for a dynamic reconfiguration, i.e. to allow to add a philosopher to the table during the execution. The rules can be specified
configuration for our dining philosopher system. We choose an initial configuration
+
using the either the graphical or tree-based [[Henshin/Graphical Editor|transformation editor]]. The graphical versions of our rules
of 3 philosophers where all forks are lying on the table. We can define this either
+
are depicted below. We have the following rules:
using a generated EMF editor for the philosophers model, or the sample reflective
+
* ''left'' and ''right'' for picking up forks (''right'' is symmetric to ''left'' )
editor. Make sure though that the Ecore modeled is regisetered in the EMF package
+
* ''release'' for putting them back on the table
registry.
+
* ''create'' for adding a new philosopher to the table.  
  
Now we are all set and ready to generate our state space. Open the ''New'' wizard
+
Adding philosophers without an upper limit would result in an infinite state space. Therefore, we include negative application conditions (NACs) in the rule ''create'' to make sure that we cannot add arbitrarily many philosophers. Here we chose an upper limit of at most 5 philosophers.
and select ''State space'' in the Henshin category. After finishing the wizard a new
+
file with the extension ''statespace'' is created and opened in the graphical state
+
space explorer.
+
  
On the right-hand side you can find control panel for the explorer. On the
+
[[Image:statespace-phil-left.png|200x100px|Rule ''left'']]
top the number of states, transitions and rules is display. Here you can also
+
[[Image:statespace-phil-release.png|200x100px|Rule ''release'']]
find two switches which influence the state space generation:
+
[[Image:statespace-phil-create.png|240x120px|Rule ''create'']]
  
* Equality: this can be either ''Ecore'' or ''Graph''. By default this is set to graph and this is also the right choice for 95% percent of the cases. Using the graph equality the state space gets signifcantly smaller and yet is fully equivalent to the original one based on Ecore equality.
+
To generate a state space, we need to specify an initial configuration. We use dynamic EMF here, that means we do not generate model classes for the EMF model. Therefore, we need to use a dynamic instance model for the initial state. To create such a dynamic instance, right-click on an ''*.ecore'' file in the package explorer and select ''Henshin -> Create Dynamic Instance''. Now open the generated ''*.xmi'' file in the Sample reflective editor of EMF and specify the initial configuration.
  
* Ignore attributes: whether to ignore attributes when comparing two states. This is disabled by default. In the future we will enable it automatically if it is save to do so.
+
== Setting up the state space ==
  
Now we need to 1) import rules to be used in the state space generation, and 2)
+
Now we set up our state space file. Open the ''New...'' wizard and select ''Henshin State space'' in the Henshin category. After finishing the wizard a new file with the extension ''statespace'' is created and opened in the graphical state space explorer.
load the initial philosophers model into the state space as an initial states.
+
You can do both of them in the context menu of the explorer, as shown below.
+
  
[[Image:statespace-setup.png|300px|x]]
+
On the right-hand side you can find control panel for the explorer. On the top, the number of states, transitions and rules is displayed. Now, from the Tasks menu in the control panel, you need to do the following things:
 +
# '''Import transformation rules''' to be used in the state space generation.
 +
# '''Load one or more initial state models''' into the state space.
  
The initial state is now the staring point for building up the state space. You
+
In our dining philosophers example, we import the rules ''left'', ''right'', ''release'' and ''create''. As initial state, we load the file from above.
can explore or ''unfold'' a state by simply double clicking on it. This will
+
create a number of follow-up states which are connected with the base state
+
using transitions.
+
  
* To enable automatic layouting, click on ''Run spring layouter'' in the ''Actions'' menu in the control panel.*
+
== Building up the state space ==
  
We can continue to unfold states by double clicking on them. States are being
+
[[Image:Statespace-explorer-phil-win32.png|300px|thumb|right|State space of reconfigurable dining philosophers]]
colored in the explorer based on the following scheme:
+
The initial state appears as a green node in the state space explorer. You can click on ''Start layouter'' in the Tasks menu on the right-hand side of the explorer to enable automatic layouting. By double clicking on a state, you can unfold this state and thereby, manually explore the state space. States are depicted using different colors:
 +
* <span style="color:green">Green</span>: initial states
 +
* <span style="color:grey">Grey</span>: explored states
 +
* <span style="color:blue">Blue</span>: open states (can be explored by double clicking on them)
 +
* <span style="color:red">Red</span>: deadlock or terminal states (no rules are applicable here)
  
* green: initial state
+
You can also let the tool do the work for you by clicking on ''Start explorer'' to automatically build up the state space. This can be combined with the automatic layouter.
* grey: an explored state
+
* blue: an open state (one that can be explored by double clicking)
+
* red: deadlock or terminal states (no rules are applicable here)
+
  
You can also let the tool do the work for you: click on ''Run state space explorer'' to automatically build up the state space.
+
After a number of steps, the state space for the philosophers example is fully generated. It should look more or less like in the screenshot on the right. Here we used graph equality without extra options.
  
After a number of steps the state space for our philosophers examples is fully generated. It should look more or less like below.
+
== Offline state space generation ==
  
 +
[[Image:Henshin-offline-statespace-generation.png|300px|thumb|Offline state space generation]]
 +
State space can be also generated outside of the graphical explorer, which is, of course, much more efficient. The offline state space generation can be invoked by clicking on ''Explore State Space'' in the ''State Space'' submenu in the context menu of state space files. On multi-core machines, a multi-threade state space exploration scheme is used, which can increase the performance by a factor, depending on the number of cores and the available memory. Note that the speed is a tradeoff between memory consumption and used time. You can also generate the state space programatically:
  
[[Image:statespace-explorer-phil.png|400px|x]]
+
<source lang="java">
 +
// Loading:
 +
StateSpaceResourceSet resourceSet = new StateSpaceResourceSet("my/working/directory");
 +
StateSpace stateSpace = resourceSet.getStateSpace("myexample.statespace");
 +
StateSpaceManager manager = StateSpaceFactory.eINSTANCE.createStateSpaceManager(stateSpace, 4);
  
 +
// Exploring:
 +
StateSpaceExplorationHelper helper = new StateSpaceExplorationHelper(manager);
 +
helper.doExploration(-1, new NullProgressMonitor());
 +
</source>
 +
You can also click on ''Properties'' in the context menu of state space files to see its details, e.g. the number of states. Note that statespace files have a binary format and can get large, depending on the size of the state space. The generator is currently able to handle state spaces with millions of states and tens of millions of transitions. You can open such big files also in the graphical explorer, but they will not be visualized anymore.
  
State space can be also generated outside of the graphical explorer. This is of course much more efficient. You can do this by clicking on ''Explore State Space'' in the ''State Space'' submenu in the context menu of statespace files. You can also click on ''Properties'' in the context menu of state space files to see some details about it. Note that statespace files have a binary format and can get rather large, depending on the size of the state space. The generator is currently able to handle state spaces with millions of states and tens of millions of transitions. You can open such big files also in the graphical explorer, but they will not be vizualized anymore.
+
== Resetting the state space ==
  
Another often used functionality is to reset a state space. This removes all derived state space (all states which are not initial). You can do this also from the context menu.
+
Another often used functionality is to reset a state space. This removes all derived state space (all states which are not initial). You can do this also from the context menu of state space files, or in the Tasks menu in the graphical explorer. You can also reset a state space programmatically:
 +
<source lang="java">
 +
manager.resetStateSpace();
 +
</source>
  
== Validation of State Spaces ==
+
== Setting properties ==
  
To validate a state space open it in the graphical explorer and make sure it is fully explored (it has no open states). Then you can use the ''Validation'' menu in the control panel to validate it.
+
[[Image:HenshinStateSpaceProperties.png|250px|thumb|Editing the state space properties]]
 +
You can influence the state space generation using properties associated to the state space. You can use an action in the control panel to change the options. Some common properties are the following: ''checkLinkOrder'' determines whether graph isomorphy of Ecore equality should be used (default is false). ''identityTypes'' is a comma-separated list of class names for which unique object IDs will be generated (required for parameterized actions). ''ignoredAttributes'' is a comma-separated list of attribute names whose values will be ignored when comparing states.
  
=== OCL Invariants ===
+
== Setting rule priorities ==
  
 +
By default, in every state the explorer tries to apply all imported rules. This an be further customized by assigning priorities to the rules. This is done using properties as explained in the previous paragraphs. All rules have per default the priority 0. If you have a rule called ''myCoolRule'' you can change its priority by setting the property ''priorityMyCoolRule'' to an integer value (can be also negative). Higher values mean higher priority. The semantics is as follows: in every state the explorer tries first to apply all rules with the highest priority. If at least one rule is applicable, then the rules with lower priorities are not applied. If none of the rules was applicable, then the rules with the next lower priority are tried to be applied, and so forth. This is essentially the approach of layered graph grammars. Note that priorities are only supported in Henshin 0.9.7 or higher.
 +
 +
== Parameterized actions ==
 +
 +
[[Image:Statespace-with-rule-params.png|250px|thumb|Parameterized actions]]
 +
In the basic version, transitions are labeled just with rule names, e.g. ''left'' and ''right'' in our simple example. A more powerful approach is also supported, which allow to parameterize the transition labels with identifiers of nodes.
 +
 +
To use parameters in the state space tools, add parameters to the rules you are using and use the parameter names as names for nodes in the rules. Then, make sure that the property ''identityTypes'' contains all types which are used as parameters of rules (see above). When you now regenerate the state space, you will see the parameters on the transition labels. These parameterized actions can be also very useful for model checking later
 +
(see the paragraph on [[#Model checking with parametrized actions|model checking with parametrized actions]]).
 +
 +
= State space analysis =
 +
 +
To analyze a generated state space, open it in the graphical explorer and make sure it is fully explored (it has no open states). Then you can use the ''Validation'' menu in the control panel to analyze it.
 +
 +
== Structural invariants in OCL ==
 +
 +
[[Image:Henshin-statespace-ocl-invariant.png|250px|thumb|OCL invariant checking in the state space explorer]]
 
You can specify OCL constraints in the validation tool in the explorer and check them for your state space. For example in the dining philosophers state space we can check the following constraint:
 
You can specify OCL constraints in the validation tool in the explorer and check them for your state space. For example in the dining philosophers state space we can check the following constraint:
  
* self.forks->size()>0
+
<pre>
 +
self.forks->size() > 0
 +
</pre>
  
 
meaning that there is always at least one fork on the table. After having selected ''OCL (invariant)'' in the drop down menu, we can simply click on ''Run'' to check the constraint. In out case this should give us a negative result. Moreover, a trace into a state which does not fullfil the constraint is automatically selected in the explorer. This gives you essentially a counterexample for your invariant.
 
meaning that there is always at least one fork on the table. After having selected ''OCL (invariant)'' in the drop down menu, we can simply click on ''Run'' to check the constraint. In out case this should give us a negative result. Moreover, a trace into a state which does not fullfil the constraint is automatically selected in the explorer. This gives you essentially a counterexample for your invariant.
  
=== Model checking with CADP and mCRL2 ===
+
== Qualitative model checking with CADP and mCRL2 ==
  
 
Full model checking of temporal properties is supported using external model checkers. For qualitative model checking you can currently use either [http://www.inrialpes.fr/vasy/cadp CADP] or [http://www.mcrl2.org mCRL2]. To use the tools in Henshin you have to install it somewhere on your computer. Note that [http://www.inrialpes.fr/vasy/cadp CADP] requires an (academic) license, whereas [http://www.mcrl2.org mCRL2] is open source.
 
Full model checking of temporal properties is supported using external model checkers. For qualitative model checking you can currently use either [http://www.inrialpes.fr/vasy/cadp CADP] or [http://www.mcrl2.org mCRL2]. To use the tools in Henshin you have to install it somewhere on your computer. Note that [http://www.inrialpes.fr/vasy/cadp CADP] requires an (academic) license, whereas [http://www.mcrl2.org mCRL2] is open source.
  
When you have installed either of the tools, make sure their ar in the system-wide PATH, so that Henshin can find them. For [http://www.inrialpes.fr/vasy/cadp CADP] you also have to define the environment variable [http://www.inrialpes.fr/vasy/cadp CADP], which should point to the directory where it is installed.
+
When you have installed either of the tools, make sure they are in the system-wide PATH, so that Henshin can find them. For [http://www.inrialpes.fr/vasy/cadp CADP] you also have to define the environment variable CADP, which should point to the directory where it is installed.
 +
 
 +
Now you can model check your state space. Both [http://www.mcrl2.org mCRL2] and [http://www.inrialpes.fr/vasy/cadp CADP] support the modal mu-calculus which has a great raw expressive power, but is also hard to read/write. As an example, freedom of deadlock can be verified using the formula:
 +
 
 +
<pre>
 +
[true*]<true>true
 +
</pre>
 +
 
 +
In our example, this should evaluate to ''false''. [http://www.inrialpes.fr/vasy/cadp CADP] moreover generates a counterexample, which is shown in the explorer (here it is a trace into one of the deadlock states). Another property that we can check is the following:
 +
 
 +
<pre>
 +
<true*>nu X.<left.right>X
 +
</pre>
 +
 
 +
which basically says: Is there an infinite sequence of the actions ''left'' and ''right''? This should evaluate to ''false''. However, if we try:
 +
 
 +
<pre>
 +
<true*>nu X.<left.right.release>X
 +
</pre>
 +
 
 +
we get ''true''. Note that in [http://www.inrialpes.fr/vasy/cadp CADP] you have to put quotes around the action names.
 +
 
 +
=== Model checking with parametrized actions ===
 +
 
 +
State space with [[#Parameterized actions|parameterized actions]] can be also analyzed. Currently, mCRL2 can be used for this. The type of the actions is induced by the parameter definitions for rules. In the following, we use the example with parameterized actions from above. We can use the parameterized actions in the model checking. For instance, consider the following formula:
 +
 
 +
<pre>
 +
[true*](forall f1,f2:Fork . exists p:Philosopher .
 +
(
 +
    [left(p,f1).right(p,f2)] (nu X. mu Y. ([release(p,f1,f2)]X && [!release(p,f1,f2)]Y)))
 +
)
 +
</pre>
 +
 
 +
It states: for all forks ''f1,f2'' there exists a philosopher, such that first ''left(p,f1)'' followed by ''right(p,f2)'' and then eventually ''release(p,f1,f2)''. This property is  satisfied in our example.
 +
 
 +
For more information on the specification language check out the [http://mcrl2.org/mcrl2/wiki/index.php?title=Language_reference/Modal_formulas mCRL2 manual] or the [http://www.inrialpes.fr/vasy/cadp/man/evaluator.html CADP manual].
 +
 
 +
See also [http://www.eclipse.org/modeling/emft/henshin/documents/henshin_mcrl2.pdf this article] on this topic. Note that the mCRL2-based approach currently does not scale very well and is limited to examples with not more than a couple of thousands of states.
 +
 
 +
 
 +
== Stochastic and probabilistic model checking with PRISM ==
 +
 
 +
Henshin supports the analysis of stochastic and probabilistic graph transformation systems using [http://www.prismmodelchecker.org PRISM model checker].
 +
 
 +
=== Stochastic graph transformation systems===
 +
 
 +
Henshin support stochastic graph transformation systems (SGTSs) as introduced by Heckel et al. Based on given user-defined rates for the transformation rules, Henshin generates a so-called continuous-time Markov chain (CTMC) in the input format of PRISM.
 +
 
 +
A standard task for CTMCs is to compute so-called steady-state probabilities for a state space. In essence, this analysis yields probabilities for your system being in a certain state.
 +
 
 +
To compute steady-state probabilities in the Henshin explorer choose the tool ''PRISM CTMC (steady-states)''. Before running this tool, you should specify application rates for all rules first. This can be done by editing the properties of the state space. For a rule called ''myRule'', its rate is specified using the property with the key ''rateMyRule''. Rates must be specified as integers or doubles. You can also define a rate based on another rate, e.g. ''rateRuleA = 1-rateRuleB''. The screenshot on the left shows some example rates.
 +
Note that you can also specify optional parameters for [http://www.prismmodelchecker.org PRISM] using the ''prismParams'' properties. Make sure that the prism executable is in your path. Now you can generate the steady-state probabilities, as shown in the screenshot on the right.
 +
 
 +
[[Image:Statespace-prism-properties.png|250px|PRISM state space properties]]
 +
[[Image:Statespace-phil-steady-states-win32.png|300px|Steady-state probabilities computed with PRISM]]
 +
 
 +
Using PRISM, we can check CSL properties for state spaces generated by Henshin. You need  to identify a set of target states for which you want to compute the probability for. We recommend to check out the very nice documentation in the [http://www.prismmodelchecker.org/manual/PropertySpecification/Introduction PRISM manual on property specification] for this. However, a standard state property supported by PRISM is "deadlock". You can compute the probability for eventually reaching a deadlock with the following formula (this will actually produce either 0 or 1):
 +
<pre>
 +
P=? [ F "deadlock" ]
 +
</pre>
 +
 
 +
To compute the probability for ending up in some specific states, e.g. in state 13 or 17, you can use this:
 +
<pre>
 +
label "target" = s=13 | s=17;
 +
P=? [ F "target" ]
 +
</pre>
 +
 
 +
You can also use OCL to specify the target states, e.g.:
 +
<pre>
 +
label "target" = <<<OCL
 +
  self.philosophers->size() > 4 and
 +
  self.philosophers->size() = self.forks->size()
 +
>>>
 +
P=? [ F "target" ]
 +
</pre>
 +
 
 +
[[Image:Henshin_statespace_plot.png|250px|thumb|right|Plot generated from a PRISM experiment]]
 +
PRISM supports a so-called [http://www.prismmodelchecker.org/manual/RunningPRISM/Experiments experiments] which are essentially a sequence of model checking runs in which one parameter is changed. Based on this approach it is possible to generate plots that show how a numerical property changes if another one is changed. This feature is also supported by the PRISM adapter in Henshin's state space tools.
 +
 
 +
The only thing that you have to do is to replace some of the concrete rates for the rules by intervals. For instance, specifying the property ''rateLeft'' as ''10:10:250'' means that PRISM will compute the result for values 10, 20, 30, ..., 250 for ''rateLeft''. You can do this with multiple parameters. In that case, you should specify which parameter is used for the X-axis. For instance, to vary the parameter ''rateLeft'' you need to set the following state space property: ''prismExperiment=rateLeft''.
 +
 
 +
The Henshin tool will invoke PRISM with the correct parameters, parse the output and generate a plot such as the one in the screenshot on the right.
 +
 
 +
=== Probabilistic graph transformation systems ===
 +
 
 +
Probabilistic graph transformation systems (PGTSs) are another quantitative model. The formal details are described in an article accepted for [http://www.informatik.uni-bremen.de/icgt2012/ ICGT 2012].
 +
 
 +
The usage principles of the tool for probabilistic transformation systems are the same as for stochastic transformation systems (see above). The only difference is how probabilistic rules and probabilities are specified.
 +
 
 +
In probabilistic graph transformation systems, rules have multiple right-hand sides, each of them annotated with a probability. In Henshin, you need to specify multiple rules with the same LHS (and nested conditions) and the same name. To specify probabilities for the different rules (RHSs), you can use the properties ''probXXX1'', ''probXXX2'', ... where ''XXX'' is the rule name with capitalized first letter (cf. the specification of rates in the stochastic case above). This is all information you need to specify. The state space tool will automatically generate a PRISM specification according to the semantics of probabilistic graph transformation systems. See also the [http://www.eclipse.org/henshin/examples.php?example=probbroadcast Probabilistic Broadcast Example].
 +
 
 +
 
 +
= State space export =
 +
 
 +
Several export formats are supported. To export a state space, either right-click on the state space file in the package explorer and choose ''State Space -> Export State Space'' or invoke use the task ''Export state space'' in the state space explorer.
 +
 
 +
== CADP (*.aut) ==
  
Now you can model check your state space. Both [http://www.mcrl2.org mCRL2] and [http://www.inrialpes.fr/vasy/cadp CADP] support the model mu-calculus which has a great raw expressive power, but is also hard to read/write. You can check deadlocks in the mu-calculus using the formula:
+
Produces an LTS in the [http://www.inrialpes.fr/vasy/cadp/man/aldebaran.html#sect6 Aldebaran format]. No parameters are required for this format.
  
* [true*] <true> true
+
== PRISM CTMC (*.sm, *.tra) ==
  
This should evaluate to false in our example. [http://www.inrialpes.fr/vasy/cadp CADP] moreover generates a counterexample which is shown in the explorer (here a trace into one of the
+
Produces a continuous-time Markov chain (CTMC) in the input format of PRISM according to the semantics of stochastic graph transformation systems. If you choose an ''*.sm'' file, the model will be exported into the PRISM specification language. If you choose a ''*.tra'' file, the model will be exported as a transition matrix, which can be more efficiently parsed by PRISM.
deadlock states).
+
  
Another property that we can check is the following:
+
As parameters, you can specify target states using OCL invariants, e.g.:
  
* <true*>nu X.<left.right>X
+
<pre>
 +
label "T1" = <<<OCL self.philosophers->size() < 2 >>>
 +
label "T2" = <<<OCL self.philosophers->size() > 3 >>>
 +
</pre>
  
which basically says: Is there an infinite sequence of the actions ''left'' and ''right''? This should evaluate to false. However, if we try:
+
== PRISM MDP (*.nm, *.tra) ==
  
* <true*>nu X.<left.right.release>X
+
Produces a Markov decision process (MDP) in the input format of PRISM according to the semantics of probabilistic graph transformation systems. If you choose an ''*.nm'' file, the model will be exported into the PRISM specification language. If you choose a ''*.tra'' file, the model will be exported as a transition matrix, which can be more efficiently parsed by PRISM.
  
we should get a true. Note that in [http://www.inrialpes.fr/vasy/cadp CADP] you have to put quotes around the action names.
+
You can use parameters as for CTMCs to specify target states.
  
=== Probabilistic Analysis with PRISM ===
+
== TiKZ (*.tex) ==
  
For a stochastic analysis of your transformation you can use the [http://www.prismmodelchecker.org PRISM model checker]. A standard task in PRISM is to compute so-called steady-state probabilities for a state space. With this you can essentially find out what the probability is for your system to be in a certain state.
+
Produces a graphical representation of the state space for LaTeX.
  
To compute steady-state probailities in the Henshin explorer choose the tool ''PRISM (steady-states)''. You can just click on run.  Now the tool will complain that you have to specify some rates. It generates a properties file for you which you can edit now to enter the rates. After having saved the properties file and clicking again on ''Run'' you should get the steady-state probabilities for your state space, as shown below.
 
  
[[Image:statespace-phil-steady-states.png|400px|x]]
+
''If you have any questions please use the [https://dev.eclipse.org/mailman/listinfo/henshin-dev henshin-dev] mailing list or [http://christiankrause.blogspot.com/ contact me] directly.''
  
If you have any questions please use the [https://dev.eclipse.org/mailman/listinfo/henshin-dev henshin-dev] mailing list or contact [http://www.cwi.nl/~koehler me] directly.
+
[[Category:Henshin]][[Category:Modeling]]

Revision as of 07:58, 7 February 2018

To verify the correctness of transformations, Henshin provides tools for generating and analyzing the state spaces of in-place model transformation. Starting from some initial state, the transformation is executed in a stepwise fashion and can be, thus, analyzed, e.g. to make sure that all intermediate states are correct fulfill some invariants.

The state space tools in Henshin currently support the following features:

Henshin State Space Explorer
  • Efficient (multi-threaded), resumable generation of explicit state spaces
  • State-based abstractions:
    • Ignoring link orders (graph isomorphy)
    • Ignoring certain attributes
    • Optional object IDs
  • Interactive state space generation and visualization
  • Extensible validation/verification framework:
    • Structural state invariant checking using OCL
    • Qualitative model checking using CADP and mCRL2
    • Probabilistic model checking using PRISM
  • Extensible export functionality:
    • TikZ (*.tex)
    • CADP (*.aut)
    • PRISM (*.sm, *.nm, *.tra etc.)

All these functionalities are integrated in a graphical state space explorer, shown on the right. They can be also invoked from the context menu for state space files or programmatically. For model checking, the state space explorer provides a uniform front-end to the above mentioned analysis tools.



State space generation

In this section, we explain how to generate a state space for a Henshin transformation.

Transformation rules and initial state

As a running example we consider the academic example of dining philosophers documented here. To make it more interesting we include a rule for a dynamic reconfiguration, i.e. to allow to add a philosopher to the table during the execution. The rules can be specified using the either the graphical or tree-based transformation editor. The graphical versions of our rules are depicted below. We have the following rules:

  • left and right for picking up forks (right is symmetric to left )
  • release for putting them back on the table
  • create for adding a new philosopher to the table.

Adding philosophers without an upper limit would result in an infinite state space. Therefore, we include negative application conditions (NACs) in the rule create to make sure that we cannot add arbitrarily many philosophers. Here we chose an upper limit of at most 5 philosophers.

Rule left Rule release Rule create

To generate a state space, we need to specify an initial configuration. We use dynamic EMF here, that means we do not generate model classes for the EMF model. Therefore, we need to use a dynamic instance model for the initial state. To create such a dynamic instance, right-click on an *.ecore file in the package explorer and select Henshin -> Create Dynamic Instance. Now open the generated *.xmi file in the Sample reflective editor of EMF and specify the initial configuration.

Setting up the state space

Now we set up our state space file. Open the New... wizard and select Henshin State space in the Henshin category. After finishing the wizard a new file with the extension statespace is created and opened in the graphical state space explorer.

On the right-hand side you can find control panel for the explorer. On the top, the number of states, transitions and rules is displayed. Now, from the Tasks menu in the control panel, you need to do the following things:

  1. Import transformation rules to be used in the state space generation.
  2. Load one or more initial state models into the state space.

In our dining philosophers example, we import the rules left, right, release and create. As initial state, we load the file from above.

Building up the state space

State space of reconfigurable dining philosophers

The initial state appears as a green node in the state space explorer. You can click on Start layouter in the Tasks menu on the right-hand side of the explorer to enable automatic layouting. By double clicking on a state, you can unfold this state and thereby, manually explore the state space. States are depicted using different colors:

  • Green: initial states
  • Grey: explored states
  • Blue: open states (can be explored by double clicking on them)
  • Red: deadlock or terminal states (no rules are applicable here)

You can also let the tool do the work for you by clicking on Start explorer to automatically build up the state space. This can be combined with the automatic layouter.

After a number of steps, the state space for the philosophers example is fully generated. It should look more or less like in the screenshot on the right. Here we used graph equality without extra options.

Offline state space generation

Offline state space generation

State space can be also generated outside of the graphical explorer, which is, of course, much more efficient. The offline state space generation can be invoked by clicking on Explore State Space in the State Space submenu in the context menu of state space files. On multi-core machines, a multi-threade state space exploration scheme is used, which can increase the performance by a factor, depending on the number of cores and the available memory. Note that the speed is a tradeoff between memory consumption and used time. You can also generate the state space programatically:

// Loading:
StateSpaceResourceSet resourceSet = new StateSpaceResourceSet("my/working/directory");
StateSpace stateSpace = resourceSet.getStateSpace("myexample.statespace");
StateSpaceManager manager = StateSpaceFactory.eINSTANCE.createStateSpaceManager(stateSpace, 4);
 
// Exploring:
StateSpaceExplorationHelper helper = new StateSpaceExplorationHelper(manager);
helper.doExploration(-1, new NullProgressMonitor());

You can also click on Properties in the context menu of state space files to see its details, e.g. the number of states. Note that statespace files have a binary format and can get large, depending on the size of the state space. The generator is currently able to handle state spaces with millions of states and tens of millions of transitions. You can open such big files also in the graphical explorer, but they will not be visualized anymore.

Resetting the state space

Another often used functionality is to reset a state space. This removes all derived state space (all states which are not initial). You can do this also from the context menu of state space files, or in the Tasks menu in the graphical explorer. You can also reset a state space programmatically:

manager.resetStateSpace();

Setting properties

Editing the state space properties

You can influence the state space generation using properties associated to the state space. You can use an action in the control panel to change the options. Some common properties are the following: checkLinkOrder determines whether graph isomorphy of Ecore equality should be used (default is false). identityTypes is a comma-separated list of class names for which unique object IDs will be generated (required for parameterized actions). ignoredAttributes is a comma-separated list of attribute names whose values will be ignored when comparing states.

Setting rule priorities

By default, in every state the explorer tries to apply all imported rules. This an be further customized by assigning priorities to the rules. This is done using properties as explained in the previous paragraphs. All rules have per default the priority 0. If you have a rule called myCoolRule you can change its priority by setting the property priorityMyCoolRule to an integer value (can be also negative). Higher values mean higher priority. The semantics is as follows: in every state the explorer tries first to apply all rules with the highest priority. If at least one rule is applicable, then the rules with lower priorities are not applied. If none of the rules was applicable, then the rules with the next lower priority are tried to be applied, and so forth. This is essentially the approach of layered graph grammars. Note that priorities are only supported in Henshin 0.9.7 or higher.

Parameterized actions

Parameterized actions

In the basic version, transitions are labeled just with rule names, e.g. left and right in our simple example. A more powerful approach is also supported, which allow to parameterize the transition labels with identifiers of nodes.

To use parameters in the state space tools, add parameters to the rules you are using and use the parameter names as names for nodes in the rules. Then, make sure that the property identityTypes contains all types which are used as parameters of rules (see above). When you now regenerate the state space, you will see the parameters on the transition labels. These parameterized actions can be also very useful for model checking later (see the paragraph on model checking with parametrized actions).

State space analysis

To analyze a generated state space, open it in the graphical explorer and make sure it is fully explored (it has no open states). Then you can use the Validation menu in the control panel to analyze it.

Structural invariants in OCL

OCL invariant checking in the state space explorer

You can specify OCL constraints in the validation tool in the explorer and check them for your state space. For example in the dining philosophers state space we can check the following constraint:

self.forks->size() > 0

meaning that there is always at least one fork on the table. After having selected OCL (invariant) in the drop down menu, we can simply click on Run to check the constraint. In out case this should give us a negative result. Moreover, a trace into a state which does not fullfil the constraint is automatically selected in the explorer. This gives you essentially a counterexample for your invariant.

Qualitative model checking with CADP and mCRL2

Full model checking of temporal properties is supported using external model checkers. For qualitative model checking you can currently use either CADP or mCRL2. To use the tools in Henshin you have to install it somewhere on your computer. Note that CADP requires an (academic) license, whereas mCRL2 is open source.

When you have installed either of the tools, make sure they are in the system-wide PATH, so that Henshin can find them. For CADP you also have to define the environment variable CADP, which should point to the directory where it is installed.

Now you can model check your state space. Both mCRL2 and CADP support the modal mu-calculus which has a great raw expressive power, but is also hard to read/write. As an example, freedom of deadlock can be verified using the formula:

[true*]<true>true

In our example, this should evaluate to false. CADP moreover generates a counterexample, which is shown in the explorer (here it is a trace into one of the deadlock states). Another property that we can check is the following:

<true*>nu X.<left.right>X

which basically says: Is there an infinite sequence of the actions left and right? This should evaluate to false. However, if we try:

<true*>nu X.<left.right.release>X

we get true. Note that in CADP you have to put quotes around the action names.

Model checking with parametrized actions

State space with parameterized actions can be also analyzed. Currently, mCRL2 can be used for this. The type of the actions is induced by the parameter definitions for rules. In the following, we use the example with parameterized actions from above. We can use the parameterized actions in the model checking. For instance, consider the following formula:

[true*](forall f1,f2:Fork . exists p:Philosopher .
(
    [left(p,f1).right(p,f2)] (nu X. mu Y. ([release(p,f1,f2)]X && [!release(p,f1,f2)]Y)))
)

It states: for all forks f1,f2 there exists a philosopher, such that first left(p,f1) followed by right(p,f2) and then eventually release(p,f1,f2). This property is satisfied in our example.

For more information on the specification language check out the mCRL2 manual or the CADP manual.

See also this article on this topic. Note that the mCRL2-based approach currently does not scale very well and is limited to examples with not more than a couple of thousands of states.


Stochastic and probabilistic model checking with PRISM

Henshin supports the analysis of stochastic and probabilistic graph transformation systems using PRISM model checker.

Stochastic graph transformation systems

Henshin support stochastic graph transformation systems (SGTSs) as introduced by Heckel et al. Based on given user-defined rates for the transformation rules, Henshin generates a so-called continuous-time Markov chain (CTMC) in the input format of PRISM.

A standard task for CTMCs is to compute so-called steady-state probabilities for a state space. In essence, this analysis yields probabilities for your system being in a certain state.

To compute steady-state probabilities in the Henshin explorer choose the tool PRISM CTMC (steady-states). Before running this tool, you should specify application rates for all rules first. This can be done by editing the properties of the state space. For a rule called myRule, its rate is specified using the property with the key rateMyRule. Rates must be specified as integers or doubles. You can also define a rate based on another rate, e.g. rateRuleA = 1-rateRuleB. The screenshot on the left shows some example rates. Note that you can also specify optional parameters for PRISM using the prismParams properties. Make sure that the prism executable is in your path. Now you can generate the steady-state probabilities, as shown in the screenshot on the right.

PRISM state space properties Steady-state probabilities computed with PRISM

Using PRISM, we can check CSL properties for state spaces generated by Henshin. You need to identify a set of target states for which you want to compute the probability for. We recommend to check out the very nice documentation in the PRISM manual on property specification for this. However, a standard state property supported by PRISM is "deadlock". You can compute the probability for eventually reaching a deadlock with the following formula (this will actually produce either 0 or 1):

P=? [ F "deadlock" ]

To compute the probability for ending up in some specific states, e.g. in state 13 or 17, you can use this:

label "target" = s=13 | s=17;
P=? [ F "target" ]

You can also use OCL to specify the target states, e.g.:

label "target" = <<<OCL 
   self.philosophers->size() > 4 and
   self.philosophers->size() = self.forks->size()
>>>
P=? [ F "target" ]
Plot generated from a PRISM experiment

PRISM supports a so-called experiments which are essentially a sequence of model checking runs in which one parameter is changed. Based on this approach it is possible to generate plots that show how a numerical property changes if another one is changed. This feature is also supported by the PRISM adapter in Henshin's state space tools.

The only thing that you have to do is to replace some of the concrete rates for the rules by intervals. For instance, specifying the property rateLeft as 10:10:250 means that PRISM will compute the result for values 10, 20, 30, ..., 250 for rateLeft. You can do this with multiple parameters. In that case, you should specify which parameter is used for the X-axis. For instance, to vary the parameter rateLeft you need to set the following state space property: prismExperiment=rateLeft.

The Henshin tool will invoke PRISM with the correct parameters, parse the output and generate a plot such as the one in the screenshot on the right.

Probabilistic graph transformation systems

Probabilistic graph transformation systems (PGTSs) are another quantitative model. The formal details are described in an article accepted for ICGT 2012.

The usage principles of the tool for probabilistic transformation systems are the same as for stochastic transformation systems (see above). The only difference is how probabilistic rules and probabilities are specified.

In probabilistic graph transformation systems, rules have multiple right-hand sides, each of them annotated with a probability. In Henshin, you need to specify multiple rules with the same LHS (and nested conditions) and the same name. To specify probabilities for the different rules (RHSs), you can use the properties probXXX1, probXXX2, ... where XXX is the rule name with capitalized first letter (cf. the specification of rates in the stochastic case above). This is all information you need to specify. The state space tool will automatically generate a PRISM specification according to the semantics of probabilistic graph transformation systems. See also the Probabilistic Broadcast Example.


State space export

Several export formats are supported. To export a state space, either right-click on the state space file in the package explorer and choose State Space -> Export State Space or invoke use the task Export state space in the state space explorer.

CADP (*.aut)

Produces an LTS in the Aldebaran format. No parameters are required for this format.

PRISM CTMC (*.sm, *.tra)

Produces a continuous-time Markov chain (CTMC) in the input format of PRISM according to the semantics of stochastic graph transformation systems. If you choose an *.sm file, the model will be exported into the PRISM specification language. If you choose a *.tra file, the model will be exported as a transition matrix, which can be more efficiently parsed by PRISM.

As parameters, you can specify target states using OCL invariants, e.g.:

label "T1" = <<<OCL self.philosophers->size() < 2 >>>
label "T2" = <<<OCL self.philosophers->size() > 3 >>>

PRISM MDP (*.nm, *.tra)

Produces a Markov decision process (MDP) in the input format of PRISM according to the semantics of probabilistic graph transformation systems. If you choose an *.nm file, the model will be exported into the PRISM specification language. If you choose a *.tra file, the model will be exported as a transition matrix, which can be more efficiently parsed by PRISM.

You can use parameters as for CTMCs to specify target states.

TiKZ (*.tex)

Produces a graphical representation of the state space for LaTeX.


If you have any questions please use the henshin-dev mailing list or contact me directly.

Copyright © Eclipse Foundation, Inc. All Rights Reserved.