Model Checking Meta Plugin
The Model Checking Meta Plugin provides the ability to validate a model with model checking techniques. You can either use the built-in model checker GEAR or register your own model checker. In the Model Checking View formulas can be checked, saved and edited.
Annotations
Graphmodel annotations
@modelchecking(parameter)
Activates the Model Checking Meta Plugin. The optional parameter has to be the path of a provider class, which extends [model name]ModelCheckingProvider
. This class isn't present until the product was generated before with the @modelchecking
Annotation.
Example
@modelchecking("info.scce.cinco.product.flowgraph.provider.Provider")
graphModel FlowGraph {
...
}
@mcDefault(parameter)
Sets the default behaviour for the inclusion of nodes, containers and edges in the checkable model and is optional. The parameter has to be one of the following options:
- include - nodes, containers and edges will be included. This is the default setting.
- exclude - nodes, containers and edges won’t be included.
The @mc
annotation which is mentioned below overrides this setting for individual nodes, containers or edges.
Example
@modelchecking
@mcDefault(exclude)
graphModel FlowGraph {
...
}
@mcFulfillmentConstraint(parameter)
Specifies in what circumstances a model fulfills a formula and is optional. The parameter has to be one of the following options:
- ALL_NODES - the model fulfills a formula, when all nodes fulfill the formula. This is the default setting.
- ANY_STARTNODE - the model fulfills a formula, when at least one start node fulfills the formula.
- EACH_STARTNODE - the model fulfills a formula, when all start nodes fulfill the formula.
Example
@modelchecking
@mcFulfillmentConstraint(ANY_STARTNODE)
graphModel FlowGraph {
...
}
Moreover you can define your own constraints by overriding the method fulfills
of the ModelcheckingProvider, which is mentioned above. As the overriding method’s priority is higher, the @mcFulfillmentConstraint
option will be ignored in this case.
@mcPreferences(parameter, ... )
Specifies various (default) options for the Model Checking View in the Cinco product instance and is optional. Multiple @mcPreferences
annotations as well as multiple parameters can be used.
The following settings can be made:
- autoCheck - can be 'true' or 'false' and sets whether auto-checking of formulas should be switched on by default. The standard value is 'true'.
- defaultModelChecker - determines the model checker selected by default. The standard value is 'GEAR', which is also selected if the specified model checker cannot be found.
- highlightColor - specifies the default highlight color and has to be an RGB value. It will be '(0,255,0)' by default. By using auto-completion, the color can be chosen with a color picker.
- highlightNodes - can be 'true' or 'false' and sets whether node highlighting should be switched on by default. The standard value is 'true'.
- highlightSubFormulas - can be 'true' or 'false' and sets whether node highlighting should be switched on by default. It can only be true, when the selected model checker supports this functionality. Otherwise it is automatically set to 'false'. The standard value is 'true'.
- selectionMode - can be 'true' or 'false' and sets whether selection mode should be switched on by default. The standard value is 'false'.
- varNamePrefix - defines the character string with which a variable name for a formula starts. The value must not be empty. The default character is '%'.
All of this values have to be assigned with the operator ':='.
Example
@modelchecking
@mcPreferences("highlightColor := (42,42,42)", "highlightSubFormulas := false")
@mcPreferences("defaultModelChecker := myModelChecker")
graphModel FlowGraph {
...
}
Node / Container annotations
All settings made with the following node- and container annotations will be inherited to extending nodes and containers.
@mcStartNode
Nodes- or containers with @mcStartNode
-annotated type definitions will be marked as start nodes in the checkable model.
Example
@mcStartNode
node Start {
...
}
@mcSupportNode
Nodes- or containers with @mcSupportNode
-annotated type definitions won’t be included into the checkable model. There will be added an edge from every predecessor to every successor instead.
Support nodes and replacement behavior can be specified in detail by overriding the following methods in the aforementioned ModelCheckingProvider:
isSupportNode
getReplacementEdges
getReplacementEdgeLabels
Example
@mcSupportNode
node SomeNode {
...
}
@mc(parameter)
The @mc
annotation overrides the settings made with the @mcDefault
annotation for individual nodes and containers. Analogous use either 'include' or 'exclude' as parameter.
Example
@mc(include)
node SomeNode{
...
}
Edge annotations
@mc(parameter)
The @mc
annotation for edges behaves in the same way as described for nodes and containers.
Attribute annotations
@mcAtomicProposition
Attributes that are annotated with @mcAtomicProposition
will be treated as atomic proposition for the checkable model. The annotated attribute has to be a primitive attribute of a node, a container or a user-defined type.
Example
node SomeNode{
@mcAtomicProposition
attr EString as name
}
@mcEdgeLabel
Attributes that are annotated with @mcEdgeLabel
will be treated as edge label for the checkable model. The annotated attribute has to be a primitive attribute of an edge or a user-defined type.
Example
edge SomeEdge{
@mcEdgeLabel
attr EString as label
}
@mcFormulas
Specifies a direct graphModel attribute as formulary. The annotated attribute has to fulfill the following conditions:
- It has to be an infinite list.
- It has to be annotated with
@readOnly
.
It is also recommended to annotate the attribute with @propertiesViewHidden
. The type of the attribute has to fulfill the following conditions:
- It has to be a user-defined type.
- It has to contain at least three attributes of the type EString.
To get the full functionality also include an attribute of the type EBoolean.
Example
@modelchecking
graphModel FlowGraph {
...
type Formula {
attr EString as varName
attr EString as expression
attr EString as description
attr Estring as toCheck
}
@readOnly
@propertiesViewHidden
@mcFormulas
attr Formula as formulas[0,*]
}
How to register a model checker
To register a model checker the plugin de.jabc.cinco.meta.plugin.modelchecking.runtime
has to be added as required plugin in the MANIFEST.MF
. The desired model checker has to implement the interface de.jabc.cinco.meta.plugin.modelchecking.runtime.modelchecker.ModelChecker
and also needs to be added in the extension de.jabc.cinco.meta.plugin.modelchecking.runtime.modelchecker
. The registered model checker can be chosen in the Model Checking View.
To simplify the implementation of a model checker, it can inherit from the classes AbstractBasicModelChecker
, which still provides the possibility to use a self-defined checkable model, or SimpleModelChecker
which uses a BasicCheckableModel
that is already defined.
To provide the functionality of highlighting unsatisfied sub formulas, the model checker has to implement the interface SubToSatProvider
.
Example
// Xtend Code
class MyModelChecker extends SimpleModelChecker{
override getName() '''My Model Checker'''
override getSatisfyingNodes(BasicCheckableModel model, String expression) throws Exception{
...
}
}
Model Checking View
The Model Checking View provides the ability to type in, save and edit formulas. It displays the result of formulas to the given model.
With the Model Checking View you can
- Type in formulas in the text field at the top
- Check the formula / all formulas in the formulary
- Add, delete and edit formulas
- Add a description to formulas (checkbox 'Description')
- Reference a formula in the text field or in other formulas with the corresponding variable name
- Check only a selection of the model (checkbox 'Selection Mode')
- See the result in the formula table and as highlighting in the model
- Select multiple formulas and display the result of the conjunction
- Show check results form the nodes perspective by selecting nodes (checkbox 'Reverse Mode')
- Choose a model checker (preferences -> 'Select Model Checker')
- Auto-check on model change (preferences -> 'Enable auto check')
- Select a highlight color (preferences -> 'Show Highlight')
- Enable / Disable the highlighting of unsatisfied sub formulas (preferences -> 'Highlight unsatisfied sub formulas')
The preferences are saved per model in the metadata folder of the workspace.
Built-in model checker GEAR
The Model Checking Meta Plugin has a built-in model checker called GEAR.
GEAR Syntax overview
In the following:
- AP is an atomic proposition and may contain anything but parentheses ( and ), or spaces if they are not enclosed in double quotes ””. Of course, double quotes are forbidden as well. If in doubt, quote.
- CONSTRAINT is a space-separated list of branch constraints which follow the same rules as atomic propositions.
- FIX is a fixpoint variable used for minimum and maximum fixpoint computations. Each FIX must be unique and the same variable may not be used in different scopes. Variables may be longer than one character.
- MACRO is any macro.
- Parentheses ( and ) can be used to explicitly group operators.
The syntax is based on symbolic expressions and is oriented at the way operators are used in LISP. Argument lists to operators that take multiple arguments are separated with spaces.
f ::= AP
| (AND f f ...)
| (OR f f ...)
| (NOT f)
| (BOX f) | (BOX CONSTRAINT f)
| (BOXB f) | (BOXB CONSTRAINT f)
| (DIA f) | (DIA CONSTRAINT f)
| (DIAB f) | (DIAB CONSTRAINT f)
| (MIN FIX f)
| (MAX FIX f)
| TRUE | FALSE
| (MACRO args)
Modal μ-calculus Operators
Syntax | Semantics |
---|---|
(BOX [CONSTRAINT] φ) | After CONSTRAINT necessarily φ (successors) |
(BOXB [CONSTRAINT] φ) | After CONSTRAINT necessarily φ (predecessors) |
(DIA [CONSTRAINT] φ) | After CONSTRAINT possibly φ (successors) |
(DIAB [CONSTRAINT] φ) | After CONSTRAINT possibly φ (predecessors) |
(MIN X φ_{X}) | Minimal fixpoint operator with fixpoint variable X |
(MAX Z φ_{Z}) | Maximal fixpoint operator with fixpoint variable Z |
(NOT φ) | All nodes not satisfying φ |
(AND φ_{1} ... φ_{n}) | All nodes that satisfy every φ_{i} |
(OR φ_{1} ... φ_{n}) | All nodes that satisfy at least one φ_{i} |
CONSTRAINT is always optional.
Fixpoint variables are required to appear somewhere in the corresponding formula, otherwise it is considered unbound and the fixpoint cannot be computed. In addition the formula must be syntactically monotone, i.e. every occurrence of the fixpoint variable falls under an even number of negations.
CTL-Operators
GEAR supports CTL operators via macros. The CTL macros currently included are as follows:
Syntax | Semantics |
---|---|
(AG [back] [infty] φ) | Always Generally φ |
(EG [back] [infty] φ) | Existential Generally φ |
(AF [back] [repeat] φ) | Always Finally φ |
(EF [back] [repeat] φ) | Existential Finally φ |
(AX [back] φ) | Always Next φ |
(EX [back] φ) | Existential Next φ |
(ASU [back] φ ψ) | Always φ (Strong) Until ψ |
(ESU [back] φ ψ) | Existential φ (Strong) Until ψ |
(AWU [back] φ ψ) | Always φ Weak Until ψ |
(EWU [back] φ ψ) | Existential φ Weak Until ψ |
(NOT φ) | All nodes not satisfying φ |
(AND φ_{1} ... φ_{n}) | All nodes that satisfy every φ_{i} |
(OR φ_{1} ... φ_{n}) | All nodes that satisfy at least one φ_{i} |
Most CTL operators shown in the table above support some parameters that allow precise control over the intended semantics. All of these parameters are optional.
- back (all operators): This tells the operator to traverse edges in backward direction, i.e. from target to source.
- infty (G operators only): This is short for infinity. This option requires infinite paths instead of finite paths, i.e. sinks are not allowed.
- repeat (F operators only): Using this option requires that the property expressed in φ must appear infinitely often, i.e. whenever the property φ is satisfied, there must be a way to again reach a node where φ holds.
The operator modifiers can be combined as in e.g. (EF back repeat good)
. This holds for nodes with predecessor paths that come across good nodes infinitely often.
Note that CTL* operators are not supported.