added TrafficLight formalism

users/(default)/Formalisms/TrafficLight/TrafficLight.metamodel

@@ -0,0 +1,313 @@
+{
+	"types": {
+		"State": [
+			{
+				"name": "name",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "initial",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "current",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"Interrupt": [
+			{
+				"name": "at",
+				"type": "int",
+				"default": 0
+			},
+			{
+				"name": "event",
+				"type": "string",
+				"default": "E"
+			},
+			{
+				"name": "current",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"TimedTransition": [
+			{
+				"name": "after",
+				"type": "int",
+				"default": 0
+			}
+		],
+		"InterruptTransition": [
+			{
+				"name": "interrupt",
+				"type": "string",
+				"default": "E"
+			}
+		],
+		"Time": [
+			{
+				"name": "clock",
+				"type": "int",
+				"default": 0
+			}
+		],
+		"AbstractInterrupt": [
+			{
+				"name": "current",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"Next": [],
+		"End": [
+			{
+				"name": "current",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"Visualisation": [
+			{
+				"name": "red",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "yellow",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "green",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"VisualisedBy": []
+	},
+	"constraints": [
+		{
+			"name": "max-one-instance",
+			"event": "pre-create",
+			"code": "getAllNodes(['/Formalisms/TrafficLight/TrafficLight/Time']).length == 0",
+			"targetType": "Time"
+		},
+		{
+			"name": "noAbstractInstances",
+			"event": "pre-create",
+			"code": "false",
+			"targetType": "AbstractInterrupt"
+		},
+		{
+			"name": "one-time-instance",
+			"event": "",
+			"targetType": "*",
+			"code": "var time_instances = getAllNodes(['/Formalisms/TrafficLight/TrafficLight/Time']);\ntime_instances.length == 1"
+		}
+	],
+	"actions": [
+		{
+			"name": "set-clock",
+			"event": "post-create",
+			"code": "setAttr('clock', 1)",
+			"targetType": "Time"
+		},
+		{
+			"name": "set-clock",
+			"event": "post-create",
+			"targetType": "*",
+			"code": "var instances = getAllNodes(['/Formalisms/TrafficLight/TrafficLight/Time']);\nconsole.log(instances.length);\nif (instances.length) {\n   setAttr('clock', 0, instances[0]);\n}"
+		}
+	],
+	"cardinalities": {
+		"State": [
+			{
+				"dir": "out",
+				"type": "TimedTransition",
+				"min": 0,
+				"max": 1
+			},
+			{
+				"dir": "out",
+				"type": "VisualisedBy",
+				"min": 1,
+				"max": 1
+			},
+			{
+				"dir": "in",
+				"type": "TimedTransition",
+				"min": "0",
+				"max": "Infinity"
+			},
+			{
+				"dir": "out",
+				"type": "InterruptTransition",
+				"min": "0",
+				"max": "Infinity"
+			},
+			{
+				"dir": "in",
+				"type": "InterruptTransition",
+				"min": "0",
+				"max": "Infinity"
+			}
+		],
+		"Interrupt": [
+			{
+				"dir": "out",
+				"type": "Next",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "in",
+				"type": "Next",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"TimedTransition": [
+			{
+				"dir": "in",
+				"type": "State",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "State",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"InterruptTransition": [
+			{
+				"dir": "in",
+				"type": "State",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "State",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"Time": [],
+		"AbstractInterrupt": [
+			{
+				"dir": "in",
+				"type": "Next",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"Next": [
+			{
+				"dir": "in",
+				"type": "Interrupt",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "AbstractInterrupt",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "Interrupt",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "End",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"End": [
+			{
+				"dir": "in",
+				"type": "Next",
+				"min": "0",
+				"max": "1"
+			}
+		],
+		"Visualisation": [
+			{
+				"dir": "in",
+				"type": "VisualisedBy",
+				"min": "0",
+				"max": "Infinity"
+			}
+		],
+		"VisualisedBy": [
+			{
+				"dir": "in",
+				"type": "State",
+				"min": "0",
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "Visualisation",
+				"min": "0",
+				"max": "1"
+			}
+		]
+	},
+	"legalConnections": {
+		"State": {
+			"State": [
+				"TimedTransition",
+				"InterruptTransition"
+			],
+			"Visualisation": [
+				"VisualisedBy"
+			]
+		},
+		"Interrupt": {
+			"AbstractInterrupt": [
+				"Next"
+			],
+			"Interrupt": [
+				"Next"
+			],
+			"End": [
+				"Next"
+			]
+		}
+	},
+	"connectorTypes": {
+		"TimedTransition": "visual",
+		"InterruptTransition": "visual",
+		"Next": "visual",
+		"VisualisedBy": "visual"
+	},
+	"types2parentTypes": {
+		"State": [],
+		"Interrupt": [
+			"AbstractInterrupt"
+		],
+		"TimedTransition": [],
+		"InterruptTransition": [],
+		"Time": [],
+		"AbstractInterrupt": [],
+		"Next": [],
+		"End": [
+			"AbstractInterrupt"
+		],
+		"Visualisation": [],
+		"VisualisedBy": [],
+		"one-time-instance": [],
+		"set-clock": []
+	}
+}

users/(default)/Formalisms/TrafficLight/TrafficLight.pattern.metamodel

@@ -0,0 +1,531 @@
+{
+	"types": {
+		"__pState": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "name",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "initial",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "current",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pInterrupt": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "at",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "event",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "current",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pTimedTransition": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "after",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pInterruptTransition": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "interrupt",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pTime": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "clock",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pAbstractInterrupt": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "current",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pNext": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			}
+		],
+		"__pEnd": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "current",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pVisualisation": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			},
+			{
+				"name": "red",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "yellow",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			},
+			{
+				"name": "green",
+				"type": "code",
+				"default": "\"[PYTHON]\"\n\"Example:\t result = True\"\n\"Example:\t result = getAttr()\"\n\n\"[JAVASCRIPT]\"\n\"Example:\t true\"\n\"Example:\t getAttr()\""
+			}
+		],
+		"__pVisualisedBy": [
+			{
+				"name": "__pLabel",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotIn",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pPivotOut",
+				"type": "string",
+				"default": ""
+			},
+			{
+				"name": "__pMatchSubtypes",
+				"type": "boolean",
+				"default": false
+			}
+		]
+	},
+	"constraints": [
+		{
+			"name": "noAbstractInstances",
+			"event": "pre-create",
+			"code": "/* comment next line to enable this constraint */\nthrow \"IgnoredConstraint\"\nfalse",
+			"targetType": "AbstractInterrupt"
+		}
+	],
+	"actions": [
+		{
+			"name": "distinctPLabels",
+			"event": "post-create",
+			"code": "if( getAttr(\"__pLabel\") == \"\" )\n{\n\tvar pLabels = getAllNodes().\n\t\t\t\t\t\t\tfilter( function(n) {return hasAttr(\"__pLabel\",n);} ).\n\t\t\t\t\t\t\t\tmap( function(n) {return getAttr(\"__pLabel\",n);} ),\n\t\t i\t\t\t= \"0\";\n\n\twhile( _utils.contains(pLabels,i) )\n\t\ti = String(parseInt(i)+1);\n\tsetAttr(\"__pLabel\",i);\n}",
+			"targetType": "*"
+		}
+	],
+	"cardinalities": {
+		"__pState": [
+			{
+				"dir": ">",
+				"type": "__pTimedTransition",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": ">",
+				"type": "__pVisualisedBy",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pTimedTransition",
+				"min": 0,
+				"max": "Infinity"
+			},
+			{
+				"dir": "in",
+				"type": "__pTimedTransition",
+				"min": 0,
+				"max": "Infinity"
+			},
+			{
+				"dir": "out",
+				"type": "__pInterruptTransition",
+				"min": 0,
+				"max": "Infinity"
+			},
+			{
+				"dir": "in",
+				"type": "__pInterruptTransition",
+				"min": 0,
+				"max": "Infinity"
+			},
+			{
+				"dir": "out",
+				"type": "__pVisualisedBy",
+				"min": 0,
+				"max": "Infinity"
+			}
+		],
+		"__pInterrupt": [
+			{
+				"dir": ">",
+				"type": "__pNext",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "<",
+				"type": "__pNext",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pNext",
+				"min": 0,
+				"max": "Infinity"
+			},
+			{
+				"dir": "in",
+				"type": "__pNext",
+				"min": 0,
+				"max": "Infinity"
+			}
+		],
+		"__pTimedTransition": [
+			{
+				"dir": "in",
+				"type": "__pState",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pState",
+				"min": 0,
+				"max": "1"
+			}
+		],
+		"__pInterruptTransition": [
+			{
+				"dir": "in",
+				"type": "__pState",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pState",
+				"min": 0,
+				"max": "1"
+			}
+		],
+		"__pTime": [],
+		"__pAbstractInterrupt": [
+			{
+				"dir": "<",
+				"type": "__pNext",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "in",
+				"type": "__pNext",
+				"min": 0,
+				"max": "Infinity"
+			}
+		],
+		"__pNext": [
+			{
+				"dir": "in",
+				"type": "__pInterrupt",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pAbstractInterrupt",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pInterrupt",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pEnd",
+				"min": 0,
+				"max": "1"
+			}
+		],
+		"__pEnd": [
+			{
+				"dir": "<",
+				"type": "__pNext",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "in",
+				"type": "__pNext",
+				"min": 0,
+				"max": "Infinity"
+			}
+		],
+		"__pVisualisation": [
+			{
+				"dir": "in",
+				"type": "__pVisualisedBy",
+				"min": 0,
+				"max": "Infinity"
+			}
+		],
+		"__pVisualisedBy": [
+			{
+				"dir": "in",
+				"type": "__pState",
+				"min": 0,
+				"max": "1"
+			},
+			{
+				"dir": "out",
+				"type": "__pVisualisation",
+				"min": 0,
+				"max": "1"
+			}
+		]
+	},
+	"legalConnections": {
+		"__pState": {
+			"__pState": [
+				"__pTimedTransition",
+				"__pInterruptTransition"
+			],
+			"__pVisualisation": [
+				"__pVisualisedBy"
+			]
+		},
+		"__pInterrupt": {
+			"__pAbstractInterrupt": [
+				"__pNext"
+			],
+			"__pInterrupt": [
+				"__pNext"
+			],
+			"__pEnd": [
+				"__pNext"
+			]
+		}
+	},
+	"connectorTypes": {
+		"__pTimedTransition": "visual",
+		"__pInterruptTransition": "visual",
+		"__pNext": "visual",
+		"__pVisualisedBy": "visual"
+	},
+	"types2parentTypes": {
+		"__pState": [],
+		"__pInterrupt": [
+			"__pAbstractInterrupt"
+		],
+		"__pTimedTransition": [],
+		"__pInterruptTransition": [],
+		"__pTime": [],
+		"__pAbstractInterrupt": [],
+		"__pNext": [],
+		"__pEnd": [
+			"__pAbstractInterrupt"
+		],
+		"__pVisualisation": [],
+		"__pVisualisedBy": []
+	}
+}

users/(default)/Formalisms/TrafficLight/Translational/TrafficLightAll.py

@@ -0,0 +1,330 @@
+from Tkinter import *  
+
+class TrafficLightGUI(Frame):
+
+  def __init__(self, behaviour, master=None, title="TrafficLight"):
+
+    self.behaviour=behaviour
+
+    # Initialize superclass
+    Frame.__init__(self, master)
+
+    # parent frame, destruction protocol
+    self.root=master
+    self.root.protocol("WM_DELETE_WINDOW", self.wmQuit)
+
+    # Initialize packer
+    self.pack(fill=BOTH, expand=1)
+
+    # Create all widgets in the Frame
+    self.__createWidgets()
+
+
+  def __createWidgets(self):
+
+    self.root.configure(bg="black")
+#   self.root.pack(side=LEFT, fill=BOTH, expand=1)
+
+    Label(self.root, text="", bg="black", 
+          height=2, width=10).pack(side=TOP, padx = 2, pady=2)
+
+    self.redLight=Label(self.root, text="", bg="red",
+                        relief=GROOVE, height=5, width=10)
+    self.redLight.pack(side=TOP, padx = 2, pady=4)
+
+    self.yellowLight=Label(self.root, text="", bg="black",
+                           relief=GROOVE, height=5, width=10)
+    self.yellowLight.pack(side=TOP, padx = 2, pady=4)
+
+    self.greenLight=Label(self.root, text="", bg="black",
+                          relief=GROOVE, height=5, width=10)
+    self.greenLight.pack(side=TOP, padx = 2, pady=4)
+
+    Label(self.root, text="",bg="black",
+          height=5, width=10).pack(side=TOP,padx=2,pady=2)
+
+# Begin generated code
+
+    Button(self.root, text="PoliceInterrupt",
+          command=self.PoliceInterruptPressed, width=10, wraplength=70).pack(side=TOP, fill=Y, padx=5, pady=2)
+
+    Button(self.root, text="Quit",
+          command=self.QuitPressed, width=10, wraplength=70).pack(side=TOP, fill=Y, padx = 5, pady = 2)
+# End generated code
+
+  # binding with behaviour
+
+# Begin generated code
+  def PoliceInterruptPressed(self):
+    self.behaviour.event("PoliceInterrupt")
+
+  def QuitPressed(self):
+    self.behaviour.event("Quit")
+# End generated code
+  
+  def wmQuit(self):
+    self.root.destroy()
+
+  # the behaviour can call these methods to change the GUI
+
+  def setGreenOn(self):
+      self.greenLight["bg"] = "green"
+
+  def setGreenOff(self):
+      self.greenLight["bg"] = "black"
+
+  def setRedOn(self):
+      self.redLight["bg"] = "red"
+
+  def setRedOff(self):
+      self.redLight["bg"] = "black"
+
+  def setYellowOn(self):
+      self.yellowLight["bg"] = "yellow"
+
+  def setYellowOff(self):
+      self.yellowLight["bg"] = "black"
+
+import sys
+
+class TrafficLightBehaviour:
+
+  def __init__(self, scale=1):
+
+    self.scale = scale
+    self.currentState = None 
+
+    self.scheduledTIMEOUT = None
+
+  def initModel(self, gui):
+
+    self.gui = gui
+
+    # Begin generated code
+    self.initState = "red"
+    self.gui.setYellowOff()   
+    self.gui.setGreenOff()   
+    self.gui.setRedOn()   
+    # If the target state has an outgoing timed transition,
+    # upon entering that target state, a timeout needs to be scheduled.
+    # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+    # before the timeout expires
+    self.scheduledTIMEOUT =  self.gui.after(self.scale*3000, self.eventTIMEOUT) 
+    # End generated code
+
+    self.currentState = self.initState
+
+  def eventTIMEOUT(self):
+    self.event("TIMEOUT")
+
+  def event(self, eventName):
+    # Note that below, setting coloured lights can be optimized by checking source
+    # and target light settings and only updating those lights that changed.
+    # In the following, the more naieve approach of re-setting all lights is taken.
+
+    # Remove a scheduled timeout, if any,
+    # to ensure that if we interrupted a transition scheduled in the future
+    # that scheduled transition is removed
+    if self.scheduledTIMEOUT is not None:
+      self.gui.after_cancel(self.scheduledTIMEOUT)
+      self.scheduledTIMEOUT = None
+    # Switch based on all states
+    if False:
+      pass
+    # for all states in the automaton 
+    # Begin generated code
+    elif self.currentState == "blinkYellow":
+      if False:      
+        pass
+      # For all transitions from this state
+      elif eventName == "Quit":
+        self.currentState = "quit" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+      elif eventName == "PoliceInterrupt":
+        self.currentState = "red" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOn()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*3000, self.eventTIMEOUT) 
+      elif eventName == "TIMEOUT": 
+        self.currentState = "blinkBlack" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*500, self.eventTIMEOUT) 
+      else:
+        print("ERROR: unexpected event %s received\n" % eventName) 
+        sys.exit(1)
+    elif self.currentState == "blinkBlack":
+      if False:      
+        pass
+      # For all transitions from this state
+      elif eventName == "Quit":
+        self.currentState = "quit" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+      elif eventName == "PoliceInterrupt":
+        self.currentState = "red" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOn()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*3000, self.eventTIMEOUT) 
+      elif eventName == "TIMEOUT": 
+        self.currentState = "blinkYellow" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOn()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*500, self.eventTIMEOUT) 
+      else:
+        print("ERROR: unexpected event %s received\n" % eventName) 
+        sys.exit(1)
+    elif self.currentState == "red":
+      if False:      
+        pass
+      # For all transitions from this state
+      elif eventName == "Quit":
+        self.currentState = "quit" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+      elif eventName == "PoliceInterrupt":
+        self.currentState = "blinkYellow" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOn()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*500, self.eventTIMEOUT) 
+      elif eventName == "TIMEOUT": 
+        self.currentState = "green" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOn()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*2000, self.eventTIMEOUT) 
+      else:
+        print("ERROR: unexpected event %s received\n" % eventName) 
+        sys.exit(1)
+    elif self.currentState == "green":
+      if False:      
+        pass
+      # For all transitions from this state
+      elif eventName == "Quit":
+        self.currentState = "quit" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+      elif eventName == "PoliceInterrupt":
+        self.currentState = "blinkYellow" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOn()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*500, self.eventTIMEOUT) 
+      elif eventName == "TIMEOUT": 
+        self.currentState = "yellow" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOn()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*1000, self.eventTIMEOUT) 
+      else:
+        print("ERROR: unexpected event %s received\n" % eventName) 
+        sys.exit(1)
+    elif self.currentState == "yellow":
+      if False:      
+        pass
+      # For all transitions from this state
+      elif eventName == "Quit":
+        self.currentState = "quit" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+      elif eventName == "PoliceInterrupt":
+        self.currentState = "blinkYellow" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOn()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOff()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*500, self.eventTIMEOUT) 
+      elif eventName == "TIMEOUT": 
+        self.currentState = "red" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellowOff()   
+        self.gui.setGreenOff()   
+        self.gui.setRedOn()   
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(self.scale*3000, self.eventTIMEOUT) 
+      else:
+        print("ERROR: unexpected event %s received\n" % eventName) 
+        sys.exit(1)
+    elif self.currentState == "quit":
+      # if no outgoing transitions: no code generated
+      pass
+    # End generated code
+    else:
+      print("ERROR: unexpected currentState %s\n" % self.currentState) 
+      sys.exit(1)
+
+if __name__=="__main__":
+  behaviour=TrafficLightBehaviour()
+
+  root=Tk()
+  # Initialize the GUI with the behaviour model as a parameter 
+  gui=TrafficLightGUI(behaviour, root)
+
+  # Be sure to initialize the behaviour model after the GUI is created
+  behaviour.initModel(gui)
+
+  # The Tkinter main event loop
+  root.mainloop()

users/(default)/Formalisms/TrafficLight/Translational/commands.txt

@@ -0,0 +1,4 @@
+load "traffic"
+dump
+context trafficLight
+load egl "traffic"

users/(default)/Formalisms/TrafficLight/Translational/metadepth.dsls

@@ -0,0 +1,2 @@
+#
+#Tue Aug 26 10:03:27 CEST 2014

users/(default)/Formalisms/TrafficLight/Translational/metadepth.properties

@@ -0,0 +1,7 @@
+#
+#Tue Aug 26 10:03:27 CEST 2014
+DIR=./
+OUT=bin/
+PATH=C\:\\Users\\Bart\\Documents\\_Research\\dsm-tp\\material\\motif\\solution\\Translational\\.
+URI=file\:/C\:/Users/Bart/Documents/_Research/dsm-tp/material/motif/solution/Translational/./
+SRL=serializers/

users/(default)/Formalisms/TrafficLight/Translational/traffic.egl

@@ -0,0 +1,8 @@
+[%
+	var basePath : String := URI + DIR;
+	var filename : String := 'TrafficLight.py';
+	var filepath : String := URI + filename;
+	var t : Template := TemplateFactory.load(basePath + 'traffic_template.egl');  
+	t.process();
+	t.generate(filepath);
+%]

users/(default)/Formalisms/TrafficLight/Translational/traffic.mdepth

@@ -0,0 +1,126 @@
+Model Traffic {
+	Node State {
+		name : String {id};
+		red : boolean = false;
+		green : boolean = false;
+		yellow : boolean = false;
+		timed : TimedTransition[0..1];
+		interrupts : InterruptTransition[*];
+	}
+
+	Node InitialState[1] : State {
+	}
+
+	Node Transition {
+		target : State;
+	}
+
+	Node TimedTransition : Transition {
+		after : int;
+	}
+
+	Node InterruptTransition : Transition {
+		interrupt : String;
+	}
+
+	Node Time[1] {
+		clock : int = 0;
+	}
+
+	Node Interrupt {
+		at : int;
+		event : String;
+		next : Interrupt[0..1];
+	}
+}
+
+Traffic trafficLight {
+	// standard routine
+	InitialState red {
+		name = "red";
+		red = true;
+		timed = toGreen;
+		interrupts = [policeManOn, terminate];
+}
+State green {
+	name = "green";
+	green = true;
+	timed = toYellow;
+		interrupts = [policeManOn, terminate];
+}
+State yellow {
+	name = "yellow";
+	yellow = true;
+	timed = toRed;
+		interrupts = [policeManOn, terminate];
+}
+TimedTransition toGreen {
+	after = 10000;
+	target = green;
+}
+TimedTransition toYellow {
+	after = 6000;
+	target = yellow;
+}
+TimedTransition toRed {
+	after = 2000;
+	target = red;
+}// blinking routine
+State blinkOn {
+	name = "blink";
+	yellow = true;
+	timed = toOff;
+	interrupts = [lightsOn, terminate];
+}
+State blinkOff {
+	name = "unblink";
+	timed = toOn;
+	interrupts = [lightsOn, terminate];
+}
+TimedTransition toOn {
+	after = 1000;
+	target = blinkOn;
+}
+TimedTransition toOff {
+	after = 1000;
+	target = blinkOff;
+}
+
+// transitions between routines
+InterruptTransition policeManOn {
+	interrupt = "Policeman";
+	target = blinkOn;
+}
+InterruptTransition lightsOn {
+	interrupt = "Light";
+	target = red;
+}
+
+// terminate
+State terminated {
+	name = "STOP";
+}
+InterruptTransition terminate {
+	interrupt = "stop";
+	target = terminated;
+}
+
+// environment
+Time t {
+}
+Interrupt i1 {
+	at = 40000;
+	event = "Policeman";
+	next = i2;
+}
+Interrupt i2 {
+	at = 	60000;
+	event = "Light";
+	next = i3;
+}
+Interrupt i3 {
+	at = 90000;
+	event = "stop";
+}
+
+}

users/(default)/Formalisms/TrafficLight/Translational/traffic_template.egl

@@ -0,0 +1,189 @@
+from Tkinter import *  
+
+class TrafficLightGUI(Frame):
+
+  def __init__(self, behaviour, master=None, title="TrafficLight"):
+
+    self.behaviour=behaviour
+
+    # Initialize superclass
+    Frame.__init__(self, master)
+
+    # parent frame, destruction protocol
+    self.root=master
+    self.root.protocol("WM_DELETE_WINDOW", self.wmQuit)
+
+    # Initialize packer
+    self.pack(fill=BOTH, expand=1)
+
+    # Create all widgets in the Frame
+    self.__createWidgets()
+
+
+  def __createWidgets(self):
+
+    self.root.configure(bg="black")
+#   self.root.pack(side=LEFT, fill=BOTH, expand=1)
+
+    Label(self.root, text="", bg="black", 
+          height=2, width=10).pack(side=TOP, padx = 2, pady=2)
+
+    self.redLight=Label(self.root, text="", bg="red",
+                        relief=GROOVE, height=5, width=10)
+    self.redLight.pack(side=TOP, padx = 2, pady=4)
+
+    self.yellowLight=Label(self.root, text="", bg="black",
+                           relief=GROOVE, height=5, width=10)
+    self.yellowLight.pack(side=TOP, padx = 2, pady=4)
+
+    self.greenLight=Label(self.root, text="", bg="black",
+                          relief=GROOVE, height=5, width=10)
+    self.greenLight.pack(side=TOP, padx = 2, pady=4)
+
+    Label(self.root, text="",bg="black",
+          height=5, width=10).pack(side=TOP,padx=2,pady=2)
+
+[% for (interrupt in InterruptTransition.allInstances().collect(t | t.interrupt)) { %]
+    Button(self.root, text="[%=interrupt %]",
+          command=self.[%=interrupt %]Pressed, width=10, wraplength=70).pack(side=TOP, fill=Y, padx=5, pady=2)
+
+[% } %]
+
+[% for (interrupt in InterruptTransition.allInstances().collect(t | t.interrupt)) { %]
+
+  # binding with behaviour
+
+  def [%=interrupt %]Pressed(self):
+    self.behaviour.event("[%=interrupt %]")
+[% } %]
+  
+  def wmQuit(self):
+    self.root.destroy()
+
+  # the behaviour can call these methods to change the GUI
+
+  def setGreenOn(self):
+      self.greenLight["bg"] = "green"
+
+  def setGreenOff(self):
+      self.greenLight["bg"] = "black"
+
+  def setRedOn(self):
+      self.redLight["bg"] = "red"
+
+  def setRedOff(self):
+      self.redLight["bg"] = "black"
+
+  def setYellowOn(self):
+      self.yellowLight["bg"] = "yellow"
+
+  def setYellowOff(self):
+      self.yellowLight["bg"] = "black"
+
+import sys
+
+class TrafficLightBehaviour:
+
+  def __init__(self, scale=1):
+
+    self.scale = scale
+    self.currentState = None 
+
+    self.scheduledTIMEOUT = None
+
+  def initModel(self, gui):
+
+    self.gui = gui
+
+[% var initialState : InitialState := InitialState.allInstances().first(); %]
+
+    self.initState = "[%=initialState.name %]"
+    self.gui.setYellow[%=initialState.yellow.toString().replace('true', 'On').replace('false', 'Off') %]()   
+    self.gui.setGreen[%=initialState.green.toString().replace('true', 'On').replace('false', 'Off') %]()   
+    self.gui.setRed[%=initialState.red.toString().replace('true', 'On').replace('false', 'Off') %]()   
+[% if (initialState.timed.isDefined()) { %]
+    # If the target state has an outgoing timed transition,
+    # upon entering that target state, a timeout needs to be scheduled.
+    # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+    # before the timeout expires
+    self.scheduledTIMEOUT =  self.gui.after(int(self.scale*[%=initialState.timed.after %]), self.eventTIMEOUT) 
+[% } %]
+    # End generated code
+
+    self.currentState = self.initState
+
+  def eventTIMEOUT(self):
+    self.event("TIMEOUT")
+
+  def event(self, eventName):
+    # Note that below, setting coloured lights can be optimized by checking source
+    # and target light settings and only updating those lights that changed.
+    # In the following, the more naieve approach of re-setting all lights is taken.
+
+    # Remove a scheduled timeout, if any,
+    # to ensure that if we interrupted a transition scheduled in the future
+    # that scheduled transition is removed
+    if self.scheduledTIMEOUT is not None:
+      self.gui.after_cancel(self.scheduledTIMEOUT)
+      self.scheduledTIMEOUT = None
+    # Switch based on all states
+    if False:
+      pass
+    # for all states in the automaton 
+    # Begin generated code
+[% for (state in State.allInstances()) { %]
+[%   ("compiling "+state).println(); %]
+    elif self.currentState == "[%=state.name %]":
+      if False:      
+        pass
+      # For all transitions from this state
+[%   for (transition in state.interrupts) { %]
+[%     ("compiling "+state+"."+transition).println(); %]
+      elif eventName == "[%=transition.interrupt %]":
+        self.currentState = "[%=transition.target.name %]" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellow[%=transition.target.yellow.toString().replace('true', 'On').replace('false', 'Off') %]()   
+        self.gui.setGreen[%=transition.target.green.toString().replace('true', 'On').replace('false', 'Off') %]()   
+        self.gui.setRed[%=transition.target.red.toString().replace('true', 'On').replace('false', 'Off') %]()
+[%     if (transition.target.timed.isDefined()) { %]
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+        self.scheduledTIMEOUT =  self.gui.after(int(self.scale*[%=transition.target.timed.after %]), self.eventTIMEOUT) 
+[%     } %] 
+[%   } %]
+[%   if (state.timed.isDefined()) { %]
+[%       ("compiling "+state+"."+state.timed).println(); %]
+      elif eventName == "TIMEOUT": 
+        self.currentState = "[%=state.timed.target.name %]" # target of the transition 
+        # The visual representation associated with the target state
+        self.gui.setYellow[%=state.timed.target.yellow.toString().replace('true', 'On').replace('false', 'Off') %]()   
+        self.gui.setGreen[%=state.timed.target.green.toString().replace('true', 'On').replace('false', 'Off') %]()   
+        self.gui.setRed[%=state.timed.target.red.toString().replace('true', 'On').replace('false', 'Off') %]()
+        # If the target state has an outgoing timed transition,
+        # upon entering that target state, a timeout needs to be scheduled.
+        # Keep track of scheduledTIMEOUT to be able to cancel it later if interrupted 
+        # before the timeout expires
+[%     if (state.timed.target.timed.isDefined()) { %]
+        self.scheduledTIMEOUT =  self.gui.after(int(self.scale*[%=state.timed.target.timed.after %]), self.eventTIMEOUT) 
+[%     } %] 
+[%   } %] 
+[% } %]
+    # End generated code
+    else:
+      print("ERROR: unexpected currentState %s\n" % self.currentState) 
+      sys.exit(1)
+
+if __name__=="__main__":
+  behaviour=TrafficLightBehaviour(0.5)
+
+  root=Tk()
+  # Initialize the GUI with the behaviour model as a parameter 
+  gui=TrafficLightGUI(behaviour, root)
+
+  # Be sure to initialize the behaviour model after the GUI is created
+  behaviour.initModel(gui)
+
+  # The Tkinter main event loop
+  root.mainloop()