The synchronized product operator coordinates models conforming to the Timed Finite State Machine (TFSM) language; a state machine language augmented with timed transitions. Briefly, the operator accepts two models conforming to TFSM as argument. It selects the events with same name, and then, it coordinates the selected events by forcing a simultaneous occurrence between events.
To run the example, we need a GEMOC studio with the BCOoL plug-in installed. In the first GEMOC studio workspace, we create new project example of TFSM language.
In the second GEMOC studio workspace, we import the project from the BCOoLExample repository in github. The project includes the needed interfaces libraries, and the operator. In addition, it includes some example models to apply the operator.
To generate the model of coordination between two TFSMs, two steps are needed. First, we compile the BCOoL spec as is shown in the picture. This generates a qvto transformation that applies between any pair of models conforming to the TFSM language (in src-gen).
Once compiled, the qvto transformation enables to generate the model of coordination between any pair of TFSM models. To do so, we select the input models (jobB.tfsm and jobA.tfsm) and we click on create ccsl coordination.
This results in the generation of a CCSL specification that includes the CCSL spec of each model plus the coordination. The specification can be executed by using TimeSquare.
The specification can be executed by using TimeSquare. Figure illustrates the partial timing output (VCD) of the execution of the whole example. In the Figure, we highlight the events that results coordinated.
The workbench also offers the possibility to obtain by exploration quantitative results on the scheduling state-space. Figure illustrate the graphical representation of the state-space for our example. The exploration results in 66 states and 3454 transitions.
The picture illustrates the application of the operators in a surveillance camera system. To coordinate the models, we have to specify a timing and hierarchical coordination between the states of the TFSM CameraEncoderControl and the activities doJPEG and doJPEG2000.
In addition, we have to synchronize the activity BatterySensor and the TFSM CameraEncoderControl by coordinating the corresponding Signals and FSMEvents. To coordination these models, we develop in the following three BCOoL operators.
In a GEMOC studio, we need in the language workbench the TFSM and the Activity language. The TFSM language must be imported from here. To get the activity language, we need to clone the following github repository. Then, in the workspace, we need to import all the projects in the folders activitydiagram/dev/gemoc_commons/ and activitydiagram/dev/gemoc_concurrent/language_workbench/. In addition, we need to import the project org.gemoc.sample.bcool.tfsmandactivityhierarchical that contains the operators. We can get this project from here. The language workbench should look as in the picture.
In the modeling workbench, we import the project org.gemoc.sample.bcool.cameracontrol from here. The modeling workbench should look as in the picture. The project includes the heterogeneous models of the surveillance camera system. Also, it contains the BFlow specification that defines how the operators defined in the BCOoL specification must be applied between the models of the camera to get a coordinated system.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the the BFlow specification. Notice that, before to launch the execution, the directory gemoc-gen should contain the generated file CameraControlFlow.xml. This file is automatically generated from the BFlow specification. In case that the file was not generated, it is necessary to edit the
BFlow specification, and then, store it. This will generate the corresponding file in the gemoc-gen directory.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.
The directory gemoc-gen contains the resulting coordinated model together with the timemodel of each individual model. The coordinated model can then be used for verification. For example, the figure illustrates the use of TimeSquare to get a VCD representation of the coordinated system. In this example, we cannot compute the state-space graph since the behavior of the coordinated model is not finite.
The picture illustrates the application of the operators in a coffee machine. To coordinate the models, we have to synchronize the activity CoffeeAlgorithm and the TFSM CoffeeCoin by coordinating the corresponding Actions and FSMEvent. In the following, we develop an operator in BCOoL to generate the coordination between these models.
In a GEMOC studio, we need in the language workbench the TFSM and Activity languages. For the TFSM language, it is only necessary to go to File, New, and then Example. In the wizard, we select the GEMOC TFSM language. To get the activity language, we need to clone the following github repository. Then, in the language workbench, we need to import all the projects from the folders activitydiagram/dev/gemoc_commons/ and activitydiagram/dev/gemoc_concurrent/language_workbench/. Finally, we have to import the bcool project org.gemoc.sample.bcool.tfsmandactivity. We can get this project from here. The language workbench should look as in the picture.
In the modeling workbench, we import the project org.gemoc.sample.bcool.coffeemachine from here. The modeling workbench should look as in the picture. The project includes the different models of the coffee machine and the bflow specification to get the coordinated model.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the bflow specification.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.
The directory gemoc-gen contains the resulting coordinated model together with the timemodel of each individual model. The coordinated model can then be used for verification. For example, the figure illustrates the use of TimeSquare to compute the state-space graph.
Figure illustrate the graphical representation of the state-space for our example. The exploration results in 39 states and 405 transitions, without deadlocks. The edges in red represents the transition that contains the events that are forced to happen simultaneously by the coordination (full graph in .dot format).
In the language workbench, we need the TFSM and SigPML languages. There are two ways to get these languages. They can be deployed by using the wizard. Or, they can be imported from here. The language workbench should look as in the picture.
Also, in the language workbench, we have to import the project that contains the BCOoL specification. This corresponds with the project named org.gemoc.sample.bcool.tfsmandsigpml. One way to get this project is by using the wizard. To do so, go to New > Example > GEMOC language workbench examples. Also, the project can be downloaded from here
In the modeling workbench, we have to import the project that contains the models of the coffee machine and the BFLoW specification. The project can get it by doing New > Example > GEMOC modeling workbench examples. Also, this project can be imported from here. The modeling workbench should look as in the picture.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the BFLoW specification used to build the coordination model and then launch the simulation.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.