Property Languages for Domain-Specific Languages: the ProMoBox Approach

On this page, the demo from this paper is explained.

Info:
In AToM³, there are models (that can be instance models or metamodels) that are saved in files that end with _MDL.py and there are formalisms that are saved in files that end with _META.py
Formalisms can be generated from metamodels.

Terminology:
<OPEN> means: CTRL-O, select model (ending with _MDL.py)
<LOAD> means: F3, select formalism (ending with _META.py)
(To avoid browsing, you can check the recently opened models (F6) or the recently loaded formalisms (F7) first.)
%USER FORMALISMS% means: the User Formalisms folder in your user area
%USER MODELS% means: the User Models folder in your user area

Set up

1. Download AToM³ from http://atom3.cs.mcgill.ca/
2. Install according to the documentation. Remember where you've set up your user area
3. Download the ProMoBox project
4. Unzip to your user area. Your User Formalisms/User Models/User External folders should be merged

How to generate the ProMoBox

1. Start AToM3
2. <OPEN> %USER FORMALISMS%/DCharts/DCharts_MDL.py. Notice that this metamodel contains static information, and dynamic information as well. The parts that are dynamic are listed in the metamodel's description (to see this, press the EDIT button) under "RUNTIME"
3. <LOAD> metamodel %USER FORMALISMS%/ProMoBox/ProMoBox_META.py
4. Press the PROMOBOXIFY button - this will create metamodel and generate formalisms for the three languages
1. Generate DESIGN formalism:
1. press OK: info message that the DESIGN metamodel is generated
2. select CD_Class3 when the DESIGN formalism is created
3. press OK: info message that code is generated for the DESIGN metamodel
2. Generate SNAPSHOT formalism:
1. press OK: info message that the SNAPSHOT metamodel is generated
2. select CD_Class3 when the SNAPSHOT formalism is created
3. press OK: info message that code is generated for the SNAPSHOT metamodel
3. Generate PROPERTY formalism:
1. press OK: info message that the PROPERTY metamodel is generated
2. Manually generate code for PROPERTY metamodel (because of bug)
1. Restart AToM3
2. <OPEN> %USER FORMALISMS%/DCharts_PROPERTY/DCharts_PROPERTY_MDL.py
3. Press the red GEN button
4. In case of an "Entity Generation Warning", press OK - this won't affect the process
5. select CD_Class3 (and CD_Association3 if you would like to create association instances in patterns) when the PROPERTY formalism is created
6. press OK: info message that code is generated for the PROPERTY metamodel
5. Close AToM3

How to run a property

1. (Re)Start AToM3
2. <OPEN> %USER MODELS%/ProMoBox_SC/Elevator_MDL.py
3. <LOAD> %USER FORMALISMS%/PromelaCompiler/PromelaCompiler_META.py
4. Press the "Make Executable" button
5. this will transform your current model into a SNAPSHOT instance, so that traces can be visualized
6. Press OK: info message that the executable model is created
7. Restart AToM3
8. <OPEN> %USER MODELS%/ProMoBox_SC/ElevatorExecutable_MDL.py (note that states have now an is_active attribute)
9. <OPEN> %USER MODELS%/ProMoBox_SC/ReachesFloor_MDL.py (possible path conflict warnings can be safely clicked away)
10. <LOAD> %USER FORMALISMS%/PromelaCompiler/PromelaCompiler_META.py (possible path conflict warnings can be safely clicked away)
11. Press the yellow SPIN compile button: this compiles the elevator model AND the property model (the resulting LTL property can be read in the console or at the bottom of the generated file)
12. Press OK: info message that Promela code is created
13. Press the green SPIN verify button: opens a dialog box for verification
14. Press "Verify!" to verify whether the model satisfies the property
15. No counter-example should be found... check the info message
16. Press "Cancel" to exit verification
17. In case of a property that yields a counter-example, press the blue SPIN debug button to visualize the trace