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