AcceptingPathsConstruct
This construct removes all paths from exploration that do not end in accepting states. Such paths result in errors when tests are generated. After removing them, the model is easier to understand, and the generated tests do not use these paths. This removal process is sometimes called slicing the model.
Syntax Definition
AcceptingPathsConstruct ::= construct accepting paths
[where NonDeterministicPathRemoval = "RemoveFullPath" | "RemoveNonAcceptingChoices" ]
for Behavior .
Remarks
There are two possible ways to remove dead paths in exploration graphs with an observable choice. An observable choice is a state with more than one outgoing event or return steps, for which some but not all of the choices can reach accepting states. The two possible ways to remove these dead paths are:
The choice state could be left in the graph with the valid choices that can result in accepting states.
Paths that are not guaranteed to reach accepting states could be removed completely. If this is done, tests never choose such paths and none of the options are tested. This approach is more suitable for the environment-unpredictability interpretation of non-determinism: only paths that can be determined to reach an accepting state remain.
Since both approaches make sense, the NonDeterministicPathRemoval switch is provided to select the latter option.
Example
The following Cord code shows the use of the AcceptingPathsConstruct.
config AConfig
{
action int Implementation.AnAction(string a);
action event void Implementation.AnEventAction(string a);
}
machine AMachine() : AConfig
{
!return AnAction
}
machine CleanupCallsMachine() : AConfig
{
construct accepting paths
where NonDeterministicPathRemoval = "RemoveFullPath"
for AMachine
}
Configuration AConfig has two action declarations: AnAction and AnEventAction. Machine AMachine inherits both of those actions from configuration AConfig and additionally specifies !return AnAction to filter out only the return actions of AnAction. By doing so it does leave the call paths of AnAction truncated. These "dead" paths can be removed from AMachine by defining a machine using the AcceptingPathsConstruct. This is shown in machine CleanupCallsMachine.
The NonDeterministicPathRemoval switch is shown in this example but actually has no effect in this case because the switch only takes effect when there is a non-deterministic (diamond) choice in the graph that spawns at least one path that ends in a non-accepting end. In that situation, the switch can be used to select whether the whole diamond and the path leading to it are removed (switch value "RemoveFullPath"), or only the non-accepting branch is removed (switch value "RemoveNonAcceptingChoices").
Example
In this example, a model has the following rule methods in its model program:
RuleOne();
RuleTwo();
RuleThree();
RuleFour();
RuleFive();
RuleSix();
The goal is to use Cord scripting to slice this model to specify a scenario with the following characteristics:
Rules
RuleOneandRuleTwoshould not be included because they distract from the intended scenario.The other rules are to be included but rules
RuleFiveandRuleSixmust always be included in order.
This scenario involves an interesting slice because it must direct exploration to look ahead; a path should not be taken if it does not contain in its future that certain ordered sequence of RuleFive followed by RuleSix. The intended slice of the model program can be achieved by ensuring that the paths to be excluded end in non-accepting states. Those paths can then be pruned using the AcceptingPathsConstruct. Here is some Cord code to show this scenario in machine ScenarioSlice.
machine ModelProgram() : Config
{
construct model program from Config
}
machine ScenarioSlice() : Config
{
construct accepting paths
for !call RuleOne* || !call RuleTwo* || ...;RuleFive;RuleSix;... || ModelProgram
}
The !call RuleOne* || !call RuleTwo* composition excludes the paths that have rules RuleOne or RuleTwo. The ...;RuleFive;RuleSix;... composition includes the paths that are, in words, "any sequence, then RuleFive immediately followed by RuleSix, then any sequence". The complete scenario is then composed with the model program, ModelProgram, using the AcceptingPathsConstruct to achieve the removal of paths not ending in an accepting state.
This example shows use of the Any Sequence UniversalBehavior operator (...), the Tight SequencingBehavior operator (;), the Synchronized ParallelBehavior operator (||), the Zero or More RepetitionBehavior operator (*), and the ModelProgramConstruct.