From a013fca768f0a079e7f07d2f7c8a09aa743f06ac Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Sat, 8 Nov 2025 10:41:41 +0100 Subject: [PATCH] update assignment (MTL property was wrong! i blame chatgpt) --- assignment.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/assignment.html b/assignment.html index 827ce77..13a80a2 100644 --- a/assignment.html +++ b/assignment.html @@ -317,12 +317,12 @@ The controller can send the following events to the plant:

Starting point

-

Use this link to the starting point for this assignment.

+

Use this link to the starting point for this assignment.

Testing your solution

To test your solution, initialize the execution, and interact with the plant UI. The execution can run in (scaled) real-time, with the ability to pause/resume.

To gain more confidence that you correctly implemented the requirements, you can write Metric Temporal Logic (MTL) properties. An example of such a property is: - 

G ((topRightPressed & (X ~topRightPressed)) -> (G[0,2000] (lightOn)))
+ 
G ((topRightPressed -> lightOn) & ((topRightPressed & (X ~topRightPressed)) -> (G[0,2000] (lightOn))))
meaning: "as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds" AKA Requirement 1.