From 2dd35ab079121c4a10a26bfb63b3d754877934c3 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Fri, 7 Nov 2025 15:09:21 +0100 Subject: [PATCH] assignment: fix property (it was wrong) + always include traces for 'true' and 'false' --- assignment.html | 4 ++-- src/App/check_property.ts | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/assignment.html b/assignment.html index 337eefc..827ce77 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 -> (lightOn U (~topRightPressed & F[0,2] lightOn)))
+ 
G ((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.

diff --git a/src/App/check_property.ts b/src/App/check_property.ts index ff6e25a..85e1cce 100644 --- a/src/App/check_property.ts +++ b/src/App/check_property.ts @@ -36,7 +36,10 @@ export async function checkProperty(plant: Plant, property: return [entry]; }, [] as {simtime: number, state: any}[]); - let traces = {} as {[key: string]: [number, any][]}; + let traces = { + 'true': [0, true] as [number, any], + 'false': [0, false] as [number, any], + } as {[key: string]: [number, any][]}; for (const {simtime, state} of cleanPlantStates) { for (const [key, value] of Object.entries(state)) { // just append