The translation process contains 3 main stages:
This stage is described in detail in the CoreParser document
All function calls made in the following stages appear in the main function named 'RunTranslation'. This function is actually the "engine" of the translation process and its implementation appears in the file wrapper.c . The call to 'RunTranslation' is made in the "root rule" derived during the parsing process. (The rule of 'begin').
In this section I will go over all commands and function calls made in 'RunTranslation' that are related to this stage:
This file will contain, after running the translator with the CDL input, remarks about problems/special actions that were taken during the translation process.
This file will contain, after running the translator, a program in Promela syntax which is equivalent to the CDL input.
Adding a Boolean global variable to the list of global variables (which is kept in CoreDataStructure->GlobalVariables) named 'Fail'. This variable is initialized to false, and is turned on inside the output program whenever a "failure" happens. A failure happens when the program "tries" to "execute" a transition, but then it finds that the 'Relation' condition that has to be held right after "executing" the transition, does not hold.
Checking whether the 'SYSTEM' module is defined by a simple collection of transitions. If so: Setting the 'Combination' of 'SYSTEM' module to a ModCombin object of type 'COMBIN_MODIN', where its 'ModuleName' field is set to "SYSTEM", meaning: This is an instantiation of the module 'SYSTEM'.
Going over all modules in the program: (all Module objects in the list of modules kept in CoreDataStructure->modules). For every module, the 'DropPC' flag is updated. This flag indicates whether the program counter in the module may be removed in the output program. A program counter may be removed under the following conditions:
Implemented by: SetDropPCInModuleSet(ModuleSet*).
Building the ModCombin tree rooted at the 'Combination' field of the "SYSTEM" module.
Implemented by: UpdateModCombinTree(ModCombin*).
Going over the tree that was built in the former stage, For every instantiated module in the program: (named, let's say, "M") its 'Instantiation' field (which was initialized to 0 during the parsing) is updated to hold the number of times M is instantiated in the program (meaning: the number of nodes in the tree such that their "ModuleName" field contains "M").
Implemented by: UpdateInstantiationsOfModules(ModCombin*).
Going over the tree and for every module named, let's say, "M", such that M is instantiated in the tree n times, where n>1: The 'NewName' field of every node such that its 'ModuleName' is "M", is set to be the string "M" , contacted with a serial number. As a result of that, in the output program, there will be n "proctype"'s named: "M_0", "M_1", .... "M_n-1".
Implemented by: CheckMultipleModuleInstants(ModCombin*)
Initializing 'TranslationData' field of every node in the tree such that its 'ModuleName' field is not null (and holds, let's say, "M"), meaning: represents an instantiation of the module "M" : This field holds a 'ModCombinData' object:
After executing this stage, the 'TranslationData' field of every node in the tree that represents an instantiation of a module named, let's say, "M", will hold a copy of all information of the module M: Its transitions, local variables, 'define' statements and 'Cojoin' expression.
All string fields still hold NULL. They will be initialized later...
Implemented by: InitTranslationData(ModCombin*).
(for more details, see the section about the data structure.)
Going over all leaves in the tree and for every leaf that represents a module named, let's say, "M", such that M consists of a program counter that may be removed during the translation: If it consists of transitions that their 'Enable' condition does not include any restrictions about the program counter state, (meaning: their "enablenes" is not dependent at all on the program counter state):
In order to remove the program counter in the output program, the leaf becomes an inner node:
It is a ModCombin object of type 'COMBIN_ASYNC'.
It has 2 sons:
One son is a leaf in the tree:
It is a ModCombin object of type 'COMBIN_MODIN'
Its 'NewName' field is M_pc:
The 'Transitions' field of its 'TranslationData' field will hold a set of copies of exactly all transitions in the module M which are dependent on the program counter state.
The second son is a leaf in the tree:
It is a ModCombin object of type 'COMBIN_MODIN'
Its 'NewName' field is M_no_pc:
The 'Transitions' field of its 'TranslationData' field will hold a set of copies of exactly all transitions in the module M which are NOT dependent on the program counter state.
Implemented by: SplitLeavesWithPC(ModCombin*)
Changing local variables to global
Going over the tree and for every inner node that represents an instantiation of a module named, let's say, "M", we go over all variables in the 'Vars' field of 'TranslationData' field of the node: (Recall this is a copy of the variable set of M) For every variable v, If at least 1 of the following conditions holds:
v is an array and passed as an actual parameter by M to some module
M passes v as an actual parameter to more than 1 modules
v becomes a global variable, by turning off the flag 'IsRelevant' of its copy in the 'Vars' field and then defining a new global variable named almost the same (unless there already exists a global variable: In that case a renaming is executed).
The reason:
If the 1st condition holds: Arrays can't be passed as actual parameters to "proctype"'s.
If the 2nd condition holds: Since actual parameters are always passed by reference in CDL,every module such that v has passed to it as a parameter has to be "aware" of every change in v's state.
Implemented by: FindSharedVars(ModCombin*)
Change defines to global (1)
Going over the tree and for every node: Turning every 'define' statement in 'Defines' field in its 'TranslationData' field to a global one.
This change is made since in Promela language, local 'define' statements are not allowed.
Implemented by: TurnLocalDefinesInModCombinToGlobal(ModCombin*)
Change defines to global (2)
Going over all not-instantiated modules in the program: For every such a module: Turning every 'define' statement in its 'Defines' fields to a global one.
Implemented by: TurnLocalDefinesInModulesToGlobal(ModuleSet*)
Updating Transitions
Going over all leaves in the tree and for every leaf that represents an instantiation of module named, let's say, "M": The 'Transitions' field of its 'TranslationData' field is updated as follows: We go over every CombTransitionNode object on its list: For every such an element: The 'Enable', 'Assigns', 'Relation' of its 'Transition' field are updated as follows:
Turning sub-expressions in 'Relation' to assignments and adding them to 'Assigns' field: The transformations:
Expression Assignment
x' → x' := true
!x' → x' := false
x' = expression → x' := expression
If the HOLD PREVIOUS flag is off in the program: For every variable/formal parameter v in the scope of M and is not assigned in 'Assigns', we add a non-deterministic assignment to v, meaning: v is assigned with a random value, suitable to its type. This is done unless v is of type 'integer': In this case, it's not possible to simulate a non-deterministic assignment since doing so means building a set of more than 65,000 values as the assigned expression to v....
Applying the Assignment Rule: This change is based on the Assignment Rule.
[ Recall:
p is logical @a&ana
X = (X1, X2, ... , Xn) is a vector that contains all variables of a program that appear in p
E = (E1, E2, ... , En) is a vector such that for every 1 <= i <= n, Ei is the assigned expression to Xi (meaning: Xi' == Ei)
The following holds: p(X' := E) -> p(X')
]
If the value of every tagged variable in the 'Relation' proposition after the transition is "executed" is well-defined: For every such a tagged variable x' (Assume its well-defined value is e): We replace every appearance of x' in 'Relation' with e. As a result of that, the 'Relation' does not contain any tagged variables anymore. Assume the expression it holds now is 'exp': The following changes are made:
'Relation' ← NULL
'Enable' ← 'Enable' AND 'exp'
That way, many failure-cases, in which the 'Relation' condition does not hold after "executing" the transition are AVOIDED.
Implemented by: UpdateTransitionsInTranslationData(ModCombin*)
Handle synchronized transitions
Going over the tree and for every 2 synchronized transitions t1 & t2: If we find a possibility to a dangerous situation, meaning: A situation in which the SAME variable is assigned in both transitions simultaneously, we "force" this synchronized transition to fail in the following manner:
Assume:
The variable is x.
In t1: x is assigned with e1.
In t2: x is assigned with e2.
We update the 'Relation' field of 'Transition' field of the CombTransitionNode object that represents t1:
'Relation' ← 'Relation' AND (x == e1)
We update the 'Relation' field of 'Transition' field of the CombTransitionNode object that represents t2:
'Relation' ← 'Relation' AND (x == e2)
Naturally, after "executing" t1 & t2 simultaneously, when checking whether the 2 'Relation' conditions of t1 & t2 hold, at least 1 of them will fail since:
(e1 != e2) -> !((x == e1) AND (x == e2)).
As a result of that, the whole synchronized transition of the program will fail.
Implemented by: CheckDoubleAssignsToVarInModCombin(ModCombin*)
Reduce 'Enable' & 'Relation' fields
Going over all leaves in the tree and for every leaf: For every CombTransitionNode element on the list of 'Transitions' field of its 'TranslationData' field: The 'Enable' & 'Relation' fields of its 'Transition' field are reduced.
The supported reductions:
!true -> false
!false -> true
(true) -> true
(false) -> false
(expr = expr) -> true
(expr = true) -> expr
(expr = false) -> !expr
(expr != expr) -> false
(expr != true) -> !expr
(expr != false) -> expr
(expr && expr) -> expr
(true && true) -> true
(true && false) -> false
(false && false) -> false
(expr && true) -> expr
(expr && false) ->false
(expr || expr) -> expr
(true || true) -> true
(true || false) -> tru
(false || false) -> false
(expr || true) -> true
(expr || false) -> expr
Implemented by: ReduceExprsInModCombin(ModCombin*)
update 'Assigns' and 'Relation' fields
Going over all leaves in the tree and for every leaf: For every CombTransitionNode element on the list of 'Transitions' field of its 'TranslationData' field: Its string fields: 'EnableCondition', 'Assigns' and 'Relation' are updated as follows:
'Assigns': It holds a string that represents, in Promela syntax, all assignments on the list of 'Assigns' of 'Transition' field of the CombTransitionNode object.
'EnableCondition': It holds a string that represents, in Promela syntax, the 'Enable' condition of 'Transition' field of the CombTransitionNode object.
'Relation': Assume the string that represents the 'Relation' condition of 'Transition' field of the object is 'str': 'Relation' will hold the following string:
"if
::str -> skip;
::else -> Fail = true;
fi;"
meaning: This string checks whether the 'Relation' condition holds. If not: 'Fail' is turned on. That indicates that the transition failed.
Implemented by: InitStringFieldsInTranslationData(ModCombin*)
handling synchronization
Going over the tree and
For every inner node of type 'COMBIN_SYNC' p:
This node represents a synchronized combination of its left sub-tree with its right sub-tree: Assume its 'SerialNum' field (which was set during the parsing stage) holds the number n: The output program will contain a definition of a global channel of 0-capacity ("rendezvous" channel) named: "q_n". The goal of this channel is to simulate the needed synchronization.
[ A rendezvous-channel is used in SPIN for synchronization: Since its capacity is 0, a 'send' action on such a channel must be executed simultaneously with a 'get' action on the same channel.]
For every transition t in the left sub-tree of p: The 'Enable' and 'Relation' fields of the CombTransitionNode that represents t are updated:
'Enable' <- 'Enable' ; q_n?0;
'Relation' <- 'Relation' ; q_n?1;
For every transition t in the right sub-tree of p: The 'Enable' and 'Relation' fields of the CombTransitionNode that represents t are updated:
'Enable' <- 'Enable' ; q_n!0;
'Relation' <- 'Relation' ; q_n!1;
As a result of that: When trying to "execute" a transition t in the left/right sub-tree: If its 'Enable' condition holds, it is blocked until some transition t' in the right/left sub-tree sends/receives 0 on the channel q_n. (That happens iff the 'Enable' condition of t' holds!). The synchronized transition will be completed iff they will both execute their assignments and validate their 'Relation' conditions. That is, because after t/t' finishes executing its assignments: If its 'Relation' does not hold: 'Fail' is turned on, and the whole program blocks. Otherwise: It is blocked until t'/t finishes executing its assignments, validate its 'Relation' and sends/receives 1 on the channel q_n. If that happens, the synchronized transition is completed.
For every inner node of type 'COMBIN_PART' p:
This node represents a partial-synchronized combination of its left sub-tree with its right sub-tree: For every pair of transitions. which have to be synchronized: Assume its 'SerialNum' fields holds the number k, and p's holds the number n: The output program will contain a definition of a global channel of 0-capacity ("rendezvous" channel) named: "q_n_k". The goal of this channel is to simulate the needed synchronization between those 2 transitions.
Assume the pair consists of the transition t in the left sub-tree and the transition t' in the right sub-tree: (Where each one of them can be a simple/synchronized transition) The 'Enable' and 'Relation' fields of the CombTransitionNode that represents t are updated:
'Enable' <- 'Enable' ; q_n_k?0;
'Relation' <- 'Relation' ; q_n_k?1;
The 'Enable' and 'Relation' fields of the CombTransitionNode that represents t' are updated:
'Enable' <- 'Enable' ; q_n_k!0;
'Relation' <- 'Relation' ; q_n_k!1;
As a result of that: When trying to "execute" the transition t/the transition t': If its 'Enable' condition holds, it is blocked until t'/t sends/receives 0 on the channel q_n_k. (That happens iff the 'Enable' condition of t'/t holds!). The synchronized transition will be completed iff they will both execute their assignments and validate their 'Relation' conditions. That is, because after t/t' finishes executing its assignments: If its 'Relation' does not hold: 'Fail' is turned on, and the whole program blocks. Otherwise: It is blocked until t'/t finishes executing its assignments, validate its 'Relation' and sends/receives 1 on the channel q_n. If that happens, the synchronized transition is completed.
Implemented by: UpdateCommunicationsInModCombin(ModCombin*)
( Full definition and implementation of the 3 new data structures can be found in the following files:
modcombindata.h combtransitionset.h combtransitionnode.h modcombindata.c combtransitionset.c combtransitionnode.c )
This struct holds an exclusive copy of the transitions,variables, 'define' statements and 'Cojoin' expression of a certain module.
Fields:
| Vars | A VariableSet object that holds a copy of 'Vars' field of the module. |
| Cojoin | An Expression object that holds a copy of 'Cojoin' field of the module. |
| Defines | A DefineVarSet object that holds a copy of 'Defines' field of the module. |
| Transitions |
A CombTransitionSet object. (a set of CombTransitionNode ) Every object in the set represents a single transition of the module |
This struct holds a list of CombTransitionNode objects:
This struct represents a certain transition:
Important Fields:
| Transition | A TransitionNode object that holds a copy of the transition. |
| EnableCondition | A string that will, eventually, hold the representation of the 'Enable' field of the transition in Promela syntax. |
| Assigns | A string that will, eventually, hold the representation of the 'Assigns' field of the transition in Promela syntax. |
| Relation | A string that will, eventually, hold the representation of the 'Relation' field of the transition in Promela syntax. |
In this stage, the whole output SPIN program is printed into the file "spin_program".
Printing All global 'define' statements and constants Every statement is printed using '#define'.
Implemented by: PrintInSPINDefines(DefineVarSet*)
Types
Printing all defined types: Supposed the type name is t:
If the t is an enumeration:
In Promela language, an enumeration is defined using "mtype". We print:
"mtype = { all values of the enumeration };
#define mtype t"
In Promela syntax, it's impossible to define mtype twice, so in cases where the input program contains n different enumeration named t1, t2, ..., tn (n>1): We print:
"mtype = { all values in ALL enumeration };
#define mtype t1
#define mtype t2
.
.
#define mtype tn"
If t is a range type:
Supposed its low end is n1 and its high end is n2 (n1 <= n2):
If (n1 >= 0):
If (n2 <= 255)
We print: "#define t byte"
Otherwise:
We print: "#define t unsigned"
Otherwise:
We print: "#define t integer"
If t is an alias to a type t':
We print: "#define t t'"
Implemented by: PrintInSPINTypeSet(TypeSet*)
Printing a "never" claim:
A never claim helps us, in Promela language, to define invariants that should hold during all possible executions. When we reach the end of the body of the 'never' claim, it means that the execution fails.
Supposed the invariant is the proposition p, a possible way to define it is:
never{
do
:: assert(p);
od;
}
What is "p" in our case ?
In CDL language, there are range types. These types can not exactly be translated, since Promela language has only 4 types (bool, int, byte, unsigned). That's why, for every variable of such a type, we need to define an invariant that says that the variable always contain a value of its type. So, "p" is a conjunction of all constrains of all variables.
Notice that arrays and local variables do not appear in the claim.
Implemented by: PrintInSPINNeverClaims(VriableSet*)
Printing definitions of all global variables:
Every global variable that has an initial value in the CDL input is initialized the same way in the SPIN output.
Every global variable that has no initial value, is initialized with a random value, suitable to its type, in 'init' proctype. This is done provided that this variable is viewed in some 'Enable' condition, or appears a right side of some assignments, or viewed in a 'Relation' of some transition whereas it does not assigned in 'Assigns'. Exception:
When the variable is of type integer, it's not practical to simulate an assignment of a random value taken from a set of size bigger than 65,000...
Implemented by: PrintInSPINVariableSet(VariableSet*, Module*, int)
Printing definitions of all rendezvous-channels mentioned earlier.
Implemented by: PrintInSPINChannelsForModCombin(ModCombin*)
Printing definitions of all not-instantiated modules.
Implemented by: PrintInSPINNotInstantiatedModules(ModuleSet*)
Printing the ModCombin tree:
For every node such that its 'ModuleName' is not null (and holds, let's say, "M"), meaning: It represents an instantiation of the module M: We create a proctype named M: (Unless M is SYSTEM -> In that case, the proctype is 'init')
Then we print:
M's Formal parameters:
Only relevant formal parameters are printed, meaning: Any parameters that their suitable actual parameters have become global variables, are not printed.
M's comments, if such exist.
M's local variables:
Every variable that has an initial value in the CDL input is initialized the same way in the SPIN output.
Every variable that has no initial value, is initialized with a random value, suitable to its type, in 'init' proctype. This is done provided that this variable is viewed in some 'Enable' condition, or appears a right side of some assignments, or viewed in a 'Relation' of some transition whereas it does not assigned in 'Assigns'.
Exception:
When the variable is of type integer: In this case it's not practical to simulate an assignment of a random value taken from a set of size bigger than 65,000...
If M is a combination of n modules: M1, M2, M3, ..., Mn: we print n 'run' commands: run(M1),...,run(Mn). All these commands appear inside an 'atomic' section,
Otherwise: (M is a collection of transitions)
If M does not contain a program counter/ its program counter can't be removed: We print a do..od structure: Every option in this structure represents a single transition in M, and looks like this:
A guard: The 'EnableCondition' field of the CombTransitionNode object that represents the transition.
The 'Assigns' field of the CombTransitionNode object.
The 'Relation' field.
The whole option appears inside an "atomic" section. That's done in order to simulate the atomicity of a single transition. Such a do..od structure is equivalent to a collection of transition in CDL since in a do..od structure, every step the 'system' chooses one of the enabled option and executes it. Since Every guard in the structure is an 'Enable 'field of a single transition, it's equivalent to choosing one of the enabled transitions.
Remark:
If M has a Cojoin expression; We print:
do
:: if
::
Cojoin -> if
:: The options here are as was described
:: before
::
fi;
fi;
od;
Otherwise:
Supposed the possible initial values of the pc are: L1, ..., Ln:
We print a if..fi structure that has n options:
Every option describes all possible sequential-executions in the
CDL input, meaning: All executions that follow possible changes in the
program counter state.
For every 1 <= i <= n:
The i'th option looks like this:
Supposed there are k transitions that their 'Enable' condition includes: "pc = Li" :
If k=1, We print an "atomic" section, which includes:
A guard: The 'EnableCondition' field of the CombTransitionNode object that represents the transition.
The 'Assigns' field of the CombTransitionNode object.
The 'Relation' field.
otherwise, We print a if..fi structure, which has k options. Every option describes a single transition and then, all possible options of progression, according to the value assigned to the pc in the transition.
Implemented by: PrintInSPINModCombin(ModCombin*)