Parameter Expansion Points
To combine constraints used in the parameter configuration with enabling conditions used in the model program, it is necessary to understand the concept of parameter expansion points. Also, there are some restrictions on the type of constraints that can be used.
Enabling Conditions and Expansion Points
In Spec Explorer, many rule methods in the model program have enabling conditions, which are written using various methods from the Condition class. This section discusses how the enabling conditions interact with constraints specified in parameter combination declarations.
The following code example shows a variation of the model program code.
static class ModelProgram
{
[Rule]
static void AddJob(string name, int time, Frequency frequency)
{
Condition.IsTrue(time % 60 == 0);
//...
}
}
The enabling condition demands that all time values be multiples of 60. If parameters are passed to the rule method that do not satisfy the condition, the action is not enabled, and the parameter combination is ignored.
By default, Spec Explorer computes all parameter combinations at the end of a rule method, which is after the declaration of any enabling condition. Parameter generation can take enabling conditions into consideration in the following ways:
The enabling condition can be restated as a constraint with the parameter configuration in the Cord script.
The point at which to perform parameter expansion can be explicitly stated. This alternative results in the following modified model program code.
static class ModelProgram
{
[Rule]
static void AddJob(string name, int time, Frequency frequency)
{
Condition.IsTrue(time % 60 == 0);
Combination.Expand(name, time, frequency);
//...
}
}
Using the Combination.Expand method in a rule method body, or in a method called from a rule method, indicates that the user wants to take control of the time at which parameter expansion should be invoked. This enables including constraints from enabling conditions into the parameter generation phase by placing those enabling conditions before the expansion point. If expansion is not called explicitly, the default expansion point is at the end of a rule method.
Using Model Collection Types to Bind Parameters
To bind the domain of a parameter based on the state of the model at the point the action is expanded, for example, in a model collection type, you can control the parameter expansion point, as in the following code example.
static class ModelProgram
{
static MapContainer<int, JobInfo> jobs;
[Rule]
static void DeleteJob(int jobId)
{
Condition.IsTrue(jobs.ContainsKey(jobId));
Combination.Expand(jobId);
//...
}
}
This code implicitly binds the possible values for jobId to the jobs contained in the jobs map. However, without the explicit expansion call, jobId would stay symbolic and never be expanded because the constraint imposed by the Condition.IsTrue statement would not be considered as part of the parameter generation of input values.
Using the Combination Class in Model Code
There is no technical restriction on calls to the Combination class directly into the rule method when the expansion point is explicitly specified. For example, the following code is valid, and the exploration result is equivalent to the Interaction machine.
static class ModelProgram
{
[Rule]
static void AddJob(string name, int time, Frequency frequency)
{
Condition.In(name, "@$^", "t.cmd", "t.exe");
Condition.In(time, -1, 60, 3600);
Combination.Interaction(name);
Combination.Interaction(time, frequency);
Combination.Expand(name, time, frequency);
}
}
Parameter selection should usually be done in the Cord configuration, and not the model program. This enables different parameter selections for the same model. However, if the parameter configuration is inherent to the behavior of the modeled system, and thus universal for all instances of the model program, the above approach is valid.
Restrictions on Code before the Expansion Point
There are restrictions regarding the kind of code that can be executed before the parameter expansion point. The rule of thumb is that any computation on parameter values before expansion must have a determined control flow. The following typical operations that have a determined control flow are allowed:
Standard operations such as ==, !=, <, >, <=, >=, and so on.
Arithmetic or bitwise operation such as +, -, &, |,^, and so on.
Field selections from structures or from compound values such as
st.forcv.f.Calls to methods in the model code.
The following operations are not determined and, therefore, are not allowed:
Boolean shortcut operators and conditional expressions such as double ampersands (
&&), double pipes (||), or question marks (?), in which the condition operand depends on a parameter.If-then-else and loop clauses in which the condition depends on a parameter.
Calls to primitive (native) methods. This includes most of the string operations, such as IndexOf, Substring, and so on.
The restriction that limits determined control flow applies only to conditions that depend on parameters. Conditions that depend on model state or other global state, even including operations with undetermined control flow, are not subject to this restriction.
It is particularly recommended not to use double ampersands (&&) and double pipes (||) in Boolean operands of the Combination class, but instead single ampersands (&) and single pipes (|).
A number of methods in Combination accept more than one Boolean operand; for example, Combination.Isolated(c1,c2) is a shortcut for Combination.Isolated(c1 & c2).
If Spec Explorer encounters an operation with undetermined control flow before the expansion point, it raises an error. The user can then either rewrite the code to use only determined operations or move the operation after the expansion point.
Suppressing Parameter Expansion
The user can decide to suppress the expansion of parameters and keep them symbolic.
A parameter is excluded from expansion if one of the following conditions holds:
Its type is marked as lazy in the configuration, using
mode T = lazy.Combination.ExcludeFromExpansion(parameter)is used.