If we synchronize two SM by using the same transition in both SM, when this transition is generated to eventb it includes:
2 guards: the start state of both SM
2 actions: the final state of both SM
But mostly of the time when we want to change the state of one instance and the state of several instances.
For instance:
ROUTE (set), ROUTE_state (attribute)
ELEMENT (set), ELEMENT_state (attribute)
ROUTE_has_ELEMENTS (relation)
If we create the SM for both variables, we will have a transition called "lockRoute" that should change the state of ROUTE_state but also change the state of all the ELEMENTS of the ROUTE.
But if we put these transition in both state machines, when we generate the code it changes the state of one single ELEMENT. Somehow we could use the info of the relation "ROUTE_has_ELEMENTS" in order to chose change all the ELEMENTS.
May it is currently possible and i did not see it.
Thanks a lot.
Best Regards
If I understand it correctly the request is for a special kind of transition that works for a set of instances?
Should it always be for all instances in the source state?
Or would you sometimes want to select a specific subset of the instances in the source state. (this would be more difficult since you need a way to define the subset).
Hello,
Yes, this is a transition that works for a set of instances.
At least for my needs it would be neccesary to have the possibility to select a subset of instances in the source state.
It very common that a main element (ROUTE) is related with several other elements (SWITCH) and a change of state in the main element will cause the change on his related elements.
For instance, "lock" one Route will have to cause the lock on his 5 switches.
A way to solve it could be to use the asossiation between both sets, for instance:
ROUTE <--> SWITCH
We could have the option to select in the SM this relation so the tool can know which points will have to change the state.
With this we can transit athomicaly the states of all the related elements in one step.