can define multiple properties. can see detailed view of chosen property.

src/App/App.css

@@ -74,9 +74,20 @@ details:has(+ details) {
   display: inline-block;
 }
 
+button {
+  background-color: #fcfcfc;
+  border: 1px lightgrey solid;
+}
+
+button:not(:disabled):hover {
+  background-color: rgba(0, 0, 255, 0.2);
+}
+
 button.active {
-  border: solid blue 2px;
+  border: solid blue 1px;
   background-color: rgba(0,0,255,0.2);
+  /* margin-right: 1px; */
+  /* margin-left: 0; */
   color: black;
 }
 
@@ -110,3 +121,21 @@ div.stackHorizontal {
   display: flex;
   flex-direction: row;
 }
+
+div.status {
+  display: inline-block;
+  vertical-align: middle;
+  background-color: grey;
+  border-radius: 50%;
+  height: 12px;
+  width: 12px;
+}
+
+div.status.violated {
+  background-color: var(--error-color);
+}
+
+div.status.satisfied {
+  background-color: forestgreen;
+}
+

src/App/App.tsx

@@ -3,26 +3,33 @@ import "./App.css";
 
 import { Dispatch, ReactElement, SetStateAction, useCallback, useEffect, useMemo, useRef, useState } from "react";
 
+import AddIcon from '@mui/icons-material/Add';
+import AutoAwesomeIcon from '@mui/icons-material/AutoAwesome';
+import DeleteOutlineIcon from '@mui/icons-material/DeleteOutline';
+import VisibilityIcon from '@mui/icons-material/Visibility';
+
+import { Statechart } from "@/statecharts/abstract_syntax";
 import { detectConnections } from "@/statecharts/detect_connections";
-import { Conns, coupledExecution, EventDestination, statechartExecution, TimedReactive } from "@/statecharts/timed_reactive";
+import { Conns, coupledExecution, statechartExecution } from "@/statecharts/timed_reactive";
 import { RuntimeError } from "../statecharts/interpreter";
 import { parseStatechart } from "../statecharts/parser";
 import { BigStep, RaisedEvent } from "../statecharts/runtime_types";
 import { getSimTime, getWallClkDelay, TimeMode } from "../statecharts/time";
 import { BottomPanel } from "./BottomPanel";
-import { usePersistentState } from "./persistent_state";
 import { PersistentDetails } from "./PersistentDetails";
+import { digitalWatchPlant } from "./Plant/DigitalWatch/DigitalWatch";
 import { dummyPlant } from "./Plant/Dummy/Dummy";
 import { microwavePlant } from "./Plant/Microwave/Microwave";
 import { Plant } from "./Plant/Plant";
+import { trafficLightPlant } from "./Plant/TrafficLight/TrafficLight";
 import { RTHistory } from "./RTHistory";
 import { ShowAST, ShowInputEvents, ShowInternalEvents, ShowOutputEvents } from "./ShowAST";
+import { InsertMode } from "./TopPanel/InsertModes";
 import { TopPanel } from "./TopPanel/TopPanel";
 import { VisualEditor, VisualEditorState } from "./VisualEditor/VisualEditor";
-import { digitalWatchPlant } from "./Plant/DigitalWatch/DigitalWatch";
-import { useEditor as useEditor } from "./useEditor";
-import { InsertMode } from "./TopPanel/InsertModes";
-import { Statechart } from "@/statecharts/abstract_syntax";
+import { checkProperty, PropertyCheckResult } from "./check_property";
+import { usePersistentState } from "./persistent_state";
+import { useEditor } from "./useEditor";
 
 export type EditHistory = {
   current: VisualEditorState,
@@ -30,11 +37,13 @@ export type EditHistory = {
   future: VisualEditorState[],
 }
 
-const plants: [string, Plant<any>][] = [
+type UniversalPlantState = {[property: string]: boolean|number};
+
+const plants: [string, Plant<any, UniversalPlantState>][] = [
   ["dummy", dummyPlant],
-  ["microwave", microwavePlant],
-  ["digital watch", digitalWatchPlant],
-  ["traffic light", trafficLightPlant],
+  ["microwave", microwavePlant as unknown as Plant<any, UniversalPlantState>],
+  ["digital watch", digitalWatchPlant as unknown as Plant<any, UniversalPlantState>],
+  ["traffic light", trafficLightPlant as unknown as Plant<any, UniversalPlantState>],
 ]
 
 export type TraceItemError = {
@@ -46,6 +55,7 @@ export type TraceItemError = {
 type CoupledState = {
   sc: BigStep,
   plant: BigStep,
+  // plantCleanState: {[prop: string]: boolean|number},
 };
 
 export type TraceItem =
@@ -53,10 +63,9 @@ export type TraceItem =
 | { kind: "bigstep", simtime: number, cause: string, state: CoupledState, outputEvents: RaisedEvent[] };
 
 export type TraceState = {
-  // executor: TimedReactive<CoupledState>,
   trace: [TraceItem, ...TraceItem[]], // non-empty
   idx: number,
-}; // <-- null if there is no trace
+};
 
 export function App() {
   const [insertMode, setInsertMode] = usePersistentState<InsertMode>("insertMode", "and");
@@ -94,7 +103,7 @@ export function App() {
       message: currentTraceItem.error.message,
       shapeUid: currentTraceItem.error.highlight[0],
     }] : [],
-  ]
+  ];
 
   const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(editorState, setEditHistory);
 
@@ -108,23 +117,7 @@ export function App() {
     }
   }, [refRightSideBar.current, autoScroll]);
 
-  // const plantConns = ast && ({
-  //   inputEvents: {
-  //     // all SC inputs are directly triggerable from outside
-  //     ...exposeStatechartInputs(ast, "sc", (eventName: string) => "debug."+eventName),
-
-  //     ...Object.fromEntries(plant.uiEvents.map(e => {
-  //       const globalName = "PLANT_UI_"+e.event;
-  //       if (plant.inputEvents.some(f => f.event === e.event)) {
-  //         return [globalName, {kind: "model", model: 'plant', eventName: e.event}];
-  //       }
-  //       if (ast.inputEvents.some(f => f.event === e.event)) {
-  //         return [globalName, {kind: "model", model: 'sc', eventName: e.event}];
-  //       }
-  //     }).filter(entry => entry !== undefined)),
-  //   },
-  //   outputEvents: {}, //autoConnect(ast, "sc", plant, "plant"),
-  // }) as Conns;
+  // coupled execution
   const cE = useMemo(() => ast && coupledExecution({
     sc: statechartExecution(ast),
     plant: plant.execution,
@@ -276,6 +269,27 @@ export function App() {
     ast && autoConnect && autoDetectConns(ast, plant, setPlantConns);
   }, [ast, plant, autoConnect]);
 
+  const [properties, setProperties] = usePersistentState<string[]>("properties", []);
+  const [propertyResults, setPropertyResults] = useState<PropertyCheckResult[] | null>(null);
+  const [activeProperty, setActiveProperty] = usePersistentState<number>("activeProperty", 0);
+
+  // if some properties change, re-evaluate them:
+  useEffect(() => {
+    let timeout: NodeJS.Timeout;
+    if (trace) {
+      setPropertyResults(null);
+      timeout = setTimeout(() => {
+        Promise.all(properties.map((property, i) => {
+          return checkProperty(plant, property, trace.trace);
+        }))
+        .then(results => {
+          setPropertyResults(results);
+        })
+      })
+    }
+    return () => clearTimeout(timeout);
+  }, [properties, trace, plant]);
+
   return <>
 
   {/* Modal dialog */}
@@ -326,12 +340,14 @@ export function App() {
             className={showExecutionTrace ? "shadowBelow" : ""}
             style={{flex: '0 0 content', backgroundColor: ''}}
           >
+            {/* State tree */}
             <PersistentDetails localStorageKey="showStateTree" initiallyOpen={true}>
               <summary>state tree</summary>
               <ul>
                 {ast && <ShowAST {...{...ast, trace, highlightActive}}/>}
               </ul>
             </PersistentDetails>
+            {/* Input events */}
             <PersistentDetails localStorageKey="showInputEvents" initiallyOpen={true}>
               <summary>input events</summary>
               {ast && <ShowInputEvents
@@ -340,14 +356,17 @@ export function App() {
                 disabled={trace===null || trace.trace[trace.idx].kind === "error"}
                 showKeys={showKeys}/>}
             </PersistentDetails>
+            {/* Internal events */}
             <PersistentDetails localStorageKey="showInternalEvents" initiallyOpen={true}>
               <summary>internal events</summary>
               {ast && <ShowInternalEvents internalEvents={ast.internalEvents}/>}
             </PersistentDetails>
+            {/* Output events */}
             <PersistentDetails localStorageKey="showOutputEvents" initiallyOpen={true}>
               <summary>output events</summary>
               {ast && <ShowOutputEvents outputEvents={ast.outputEvents}/>}
             </PersistentDetails>
+            {/* Plant */}
             <PersistentDetails localStorageKey="showPlant" initiallyOpen={true}>
               <summary>plant</summary>
               <select
@@ -360,18 +379,49 @@ export function App() {
               </select>
               <br/>
               {/* Render plant */}
-              {<plant.render state={plantState} speed={speed}
+              {<plant.render state={plant.cleanupState(plantState)} speed={speed}
                 raiseUIEvent={e => onRaise("plant.ui."+e.name, e.param)}
                 />}
             </PersistentDetails>
-              <PersistentDetails localStorageKey="showConnEditor" initiallyOpen={false}>
-                <summary>connections</summary>
-                <button title="auto-connect (name-based)" className={autoConnect?"active":""}
-                  onClick={() => setAutoConnect(c => !c)}>
-                  <AutoAwesomeIcon fontSize="small"/>
+            {/* Connections */}
+            <PersistentDetails localStorageKey="showConnEditor" initiallyOpen={false}>
+              <summary>connections</summary>
+              <button title="auto-connect (name-based)" className={autoConnect?"active":""}
+                onClick={() => setAutoConnect(c => !c)}>
+                <AutoAwesomeIcon fontSize="small"/>
+              </button>
+              {ast && ConnEditor(ast, plant, plantConns, setPlantConns)}
+            </PersistentDetails>
+            {/* Properties */}
+            <PersistentDetails localStorageKey="showProperty" initiallyOpen={false}>
+              <summary>properties</summary>
+              <div className="toolbar">
+                <button title="add property" onClick={() => setProperties(properties => [...properties, ""])}>
+                  <AddIcon fontSize="small"/>
                 </button>
-                {ast && ConnEditor(ast, plant, plantConns, setPlantConns)}
-              </PersistentDetails>
+              </div>
+              {properties.map((property, i) => {
+                const result = propertyResults && propertyResults[i];
+                let violated = null, propertyError = null;
+                if (result) {
+                  violated = result[0] && !result[0][0].satisfied;
+                  propertyError = result[1];
+                }
+                return <div style={{width:'100%'}} key={i} className="toolbar">
+                  <div className={"status" + (violated === null ? "" : (violated ? " violated" : " satisfied"))}></div>
+                  &nbsp;
+                  <button title="see in trace (below)" className={activeProperty === i ? "active" : ""} onClick={() => setActiveProperty(i)}>
+                    <VisibilityIcon fontSize="small"/>
+                  </button>
+                  <input type="text" style={{width:'calc(97% - 70px)'}} value={property} onChange={e => setProperties(properties => properties.toSpliced(i, 1, e.target.value))}/>
+                  <button title="delete this property" onClick={() => setProperties(properties => properties.toSpliced(i, 1))}>
+                    <DeleteOutlineIcon fontSize="small"/>
+                  </button>
+                  {propertyError && <div style={{color: 'var(--error-color)'}}>{propertyError}</div>}
+                </div>;
+              })}
+            </PersistentDetails>
+            {/* Traces */}
 
             <details open={showExecutionTrace} onToggle={e => setShowExecutionTrace(e.newState === "open")}><summary>execution trace</summary>
               <input id="checkbox-show-plant-items" type="checkbox" checked={showPlantTrace} onChange={e => setShowPlantTrace(e.target.checked)}/>
@@ -390,7 +440,8 @@ export function App() {
               // minHeight: '75%', // <-- allows us to always scroll down the sidebar far enough such that the execution history is enough in view
               }}>
                 <div ref={refRightSideBar}>
-                  {ast && <RTHistory {...{ast, trace, setTrace, setTime, showPlantTrace}}/>}
+                  {ast && <RTHistory {...{ast, trace, setTrace, setTime, showPlantTrace,
+                    propertyTrace: propertyResults && propertyResults[activeProperty] && propertyResults[activeProperty][0] || []}}/>}
                 </div>
             </div>}
           <div style={{flex: '0 0 content'}}>
@@ -407,32 +458,7 @@ export function App() {
   </>;
 }
 
-function ShowEventDestination(dst: EventDestination) {
-  if (dst.kind === "model") {
-    return <>{dst.model}.{dst.eventName}</>;
-  }
-  else if (dst.kind === "output") {
-    return <>{dst.eventName}</>;
-  }
-  else {
-    return <>&#x1F5D1;</>; // <-- garbage can icon
-  }
-}
-
-function ShowConns({inputEvents, outputEvents}: Conns) {
-  return <div>
-    {/* <div style={{color: "grey"}}>
-      {Object.entries(inputEvents).map(([eventName, destination]) => <div>{eventName} &#x2192; <ShowEventDestination {...destination}/></div>)}
-    </div>
-    {Object.entries(outputEvents).map(([modelName, mapping]) => <>{Object.entries(mapping).map(([eventName, destination]) => <div>{modelName}.{eventName} &#x2192; <ShowEventDestination {...destination}/></div>)}</>)} */}
-  </div>;
-}
-
-import AutoFixHighIcon from '@mui/icons-material/AutoFixHigh';
-import AutoAwesomeIcon from '@mui/icons-material/AutoAwesome';
-import { trafficLightPlant } from "./Plant/TrafficLight/TrafficLight";
-
-function autoDetectConns(ast: Statechart, plant: Plant<any>, setPlantConns: Dispatch<SetStateAction<Conns>>) {
+function autoDetectConns(ast: Statechart, plant: Plant<any, any>, setPlantConns: Dispatch<SetStateAction<Conns>>) {
   for (const {event: a} of plant.uiEvents) {
     for (const {event: b} of plant.inputEvents) {
       if (a === b) {
@@ -462,7 +488,8 @@ function autoDetectConns(ast: Statechart, plant: Plant<any>, setPlantConns: Disp
   }
 }
 
-function ConnEditor(ast: Statechart, plant: Plant<any>, plantConns: Conns, setPlantConns: Dispatch<SetStateAction<Conns>>) {
+
+function ConnEditor(ast: Statechart, plant: Plant<any, any>, plantConns: Conns, setPlantConns: Dispatch<SetStateAction<Conns>>) {
   const plantInputs = <>{plant.inputEvents.map(e => <option key={'plant.'+e.event} value={'plant.'+e.event}>plant.{e.event}</option>)}</>
   const scInputs = <>{ast.inputEvents.map(e => <option key={'sc.'+e.event} value={'sc.'+e.event}>sc.{e.event}</option>)}</>;
   return <>
@@ -473,7 +500,8 @@ function ConnEditor(ast: Statechart, plant: Plant<any>, plantConns: Conns, setPl
       <select id={`select-dst-sc-${e}`}
         style={{width:'50%'}}
         value={plantConns['sc.'+e]?.join('.')}
-        onChange={domEvent => setPlantConns(conns => ({...conns, [`sc.${e}`]: domEvent.target.value.split('.') as [string,string]}))}>
+        // @ts-ignore
+        onChange={domEvent => setPlantConns(conns => ({...conns, [`sc.${e}`]: (domEvent.target.value === "" ? undefined : (domEvent.target.value.split('.') as [string,string]))}))}>
         <option key="none" value=""></option>
         {plantInputs}
       </select>
@@ -485,7 +513,8 @@ function ConnEditor(ast: Statechart, plant: Plant<any>, plantConns: Conns, setPl
       <select id={`select-dst-plant-${e.event}`}
         style={{width:'50%'}}
         value={plantConns['plant.'+e.event]?.join('.')}
-        onChange={(domEvent => setPlantConns(conns => ({...conns, [`plant.${e.event}`]: domEvent.target.value.split('.') as [string,string]})))}>
+        // @ts-ignore
+        onChange={(domEvent => setPlantConns(conns => ({...conns, [`plant.${e.event}`]: (domEvent.target.value === "" ? undefined : (domEvent.target.value.split('.') as [string,string]))})))}>
         <option key="none" value=""></option>
         {scInputs}
       </select>
@@ -497,7 +526,8 @@ function ConnEditor(ast: Statechart, plant: Plant<any>, plantConns: Conns, setPl
       <select id={`select-dst-plant-ui-${e.event}`}
         style={{width:'50%'}}
         value={plantConns['plant.ui.'+e.event]?.join('.')}
-        onChange={domEvent => setPlantConns(conns => ({...conns, [`plant.ui.${e.event}`]: domEvent.target.value.split('.') as [string,string]}))}>
+        // @ts-ignore
+        onChange={domEvent => setPlantConns(conns => ({...conns, [`plant.ui.${e.event}`]: (domEvent.target.value === "" ? undefined : (domEvent.target.value.split('.') as [string,string]))}))}>
         <option key="none" value=""></option>
         {scInputs}
         {plantInputs}

src/App/Plant/DigitalWatch/DigitalWatch.tsx

@@ -3,7 +3,7 @@ import { ConcreteSyntax } from "@/App/VisualEditor/VisualEditor";
 import { detectConnections } from "@/statecharts/detect_connections";
 import { parseStatechart } from "@/statecharts/parser";
 import { RT_Statechart } from "@/statecharts/runtime_types";
-import { useEffect } from "react";
+import { memo, useEffect } from "react";
 import { makeStatechartPlant, PlantRenderProps } from "../Plant";
 
 import dwatchConcreteSyntax from "./model.json";
@@ -12,6 +12,7 @@ import digitalFont from "./digital-font.ttf";
 import "./DigitalWatch.css";
 import imgNote from "./noteSmall.png";
 import imgWatch from "./watch.png";
+import { objectsEqual } from "@/util/util";
 
 export const [dwatchAbstractSyntax, dwatchErrors] = parseStatechart(dwatchConcreteSyntax as ConcreteSyntax, detectConnections(dwatchConcreteSyntax as ConcreteSyntax));
 
@@ -20,33 +21,66 @@ if (dwatchErrors.length > 0) {
   throw new Error("there were errors parsing dwatch plant model. see console.")
 }
 
+export type DigitalWatchPlantState = {
+  lightOn: boolean,
+  beep: boolean,
+  alarmOn: boolean,
+  displayingTime: boolean,
+  displayingAlarm: boolean,
+  displayingChrono: boolean,
+  hideH: boolean,
+  hideM: boolean,
+  hideS: boolean,
+  h: number,
+  m: number,
+  s: number,
+  ah: number,
+  am: number,
+  as: number,
+  cm: number,
+  cs: number,
+  chs: number,
+
+  // these properties are true for as long as the mouse button is down:
+  topLeftPressed: boolean,
+  topRightPressed: boolean,
+  bottomRightPressed: boolean,
+  bottomLeftPressed: boolean,
+}
+
+function dwatchConfigToState(rtConfig: RT_Statechart): DigitalWatchPlantState {
+  return {
+    lightOn: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("lightOn")!.uid),
+    beep: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("beep")!.uid),
+    alarmOn: rtConfig.environment.get("alarm"),
+    displayingTime: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("displayingTime")!.uid),
+    displayingAlarm: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("displayingAlarm")!.uid),
+    displayingChrono: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("displayingChrono")!.uid),
+    hideH: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("hideH")!.uid),
+    hideM: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("hideM")!.uid),
+    hideS: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("hideS")!.uid),
+    h: rtConfig.environment.get("h"),
+    m: rtConfig.environment.get("m"),
+    s: rtConfig.environment.get("s"),
+    ah: rtConfig.environment.get("ah"),
+    am: rtConfig.environment.get("am"),
+    as: rtConfig.environment.get("as"),
+    cm: rtConfig.environment.get("cm"),
+    cs: rtConfig.environment.get("cs"),
+    chs: rtConfig.environment.get("chs"),
+
+    topLeftPressed: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("topLeftPressed")!.uid),
+    topRightPressed: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("topRightPressed")!.uid),
+    bottomRightPressed: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("bottomRightPressed")!.uid),
+    bottomLeftPressed: rtConfig.mode.has(dwatchAbstractSyntax.label2State.get("bottomLeftPressed")!.uid),
+
+  }
+}
+
 
 const twoDigits = (n: number) => ("0"+n.toString()).slice(-2);
 
-export function DigitalWatch({state, speed, raiseUIEvent}: PlantRenderProps<RT_Statechart>) {
-  const displayingTime = state.mode.has("625");
-  const displayingAlarm = state.mode.has("626");
-  const displayingChrono = state.mode.has("624");
-
-  const lightOn = state.mode.has("630");
-
-  const alarm = state.environment.get("alarm");
-
-  const h = state.environment.get("h");
-  const m = state.environment.get("m");
-  const s = state.environment.get("s");
-  const ah = state.environment.get("ah");
-  const am = state.environment.get("am");
-  const as = state.environment.get("as");
-  const cm = state.environment.get("cm");
-  const cs = state.environment.get("cs");
-  const chs = state.environment.get("chs");
-
-  const hideH = state.mode.has("628");
-  const hideM = state.mode.has("633");
-  const hideS = state.mode.has("627");
-
-  // console.log({cm,cs,chs});
+export const DigitalWatch = memo(function DigitalWatch({state: {displayingTime, displayingAlarm, displayingChrono, lightOn, alarmOn, beep, h, m, s, ah, am, as, cm, cs, chs, hideH, hideM, hideS}, speed, raiseUIEvent}: PlantRenderProps<DigitalWatchPlantState>) {
 
   let hhmmss;
   if (displayingTime) {
@@ -63,8 +97,6 @@ export function DigitalWatch({state, speed, raiseUIEvent}: PlantRenderProps<RT_S
 
   preloadAudio(sndBeep);
 
-  const beep = state.mode.has("632");
-
   useEffect(() => {
     if (beep) {
       playSound(sndBeep, false);
@@ -87,40 +119,41 @@ export function DigitalWatch({state, speed, raiseUIEvent}: PlantRenderProps<RT_S
       <text x="111" y="126" dominantBaseline="middle" textAnchor="middle" fontFamily="digital-font" fontSize={28} style={{whiteSpace:'preserve'}}>{hhmmss}</text>
     
       <rect className="watchButtonHelper" x={0} y={54} width={24} height={24} 
-        onMouseDown={() => raiseUIEvent({name: "topLeftPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "topLeftReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "topLeftMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "topLeftMouseUp"})}
       />
       <rect className="watchButtonHelper" x={198} y={54} width={24} height={24}
-        onMouseDown={() => raiseUIEvent({name: "topRightPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "topRightReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "topRightMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "topRightMouseUp"})}
       />
       <rect className="watchButtonHelper" x={0} y={154} width={24} height={24}
-        onMouseDown={() => raiseUIEvent({name: "bottomLeftPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "bottomLeftReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "bottomLeftMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "bottomLeftMouseUp"})}
       />
       <rect className="watchButtonHelper" x={198} y={154} width={24} height={24}
-        onMouseDown={() => raiseUIEvent({name: "bottomRightPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "bottomRightReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "bottomRightMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "bottomRightMouseUp"})}
       />
 
-      {alarm &&
+      {alarmOn &&
         <image x="54" y="98" xlinkHref={imgNote} />
       }
     </svg>
   </>;
-}
+}, objectsEqual);
 
 export const digitalWatchPlant = makeStatechartPlant({
   ast: dwatchAbstractSyntax,
+  cleanupState: dwatchConfigToState,
   render: DigitalWatch,
   uiEvents: [
-    { kind: "event", event: "topLeftPressed" },
-    { kind: "event", event: "topRightPressed" },
-    { kind: "event", event: "bottomRightPressed" },
-    { kind: "event", event: "bottomLeftPressed" },
-    { kind: "event", event: "topLeftReleased" },
-    { kind: "event", event: "topRightReleased" },
-    { kind: "event", event: "bottomRightReleased" },
-    { kind: "event", event: "bottomLeftReleased" },
+    { kind: "event", event: "topLeftMouseDown" },
+    { kind: "event", event: "topRightMouseDown" },
+    { kind: "event", event: "bottomRightMouseDown" },
+    { kind: "event", event: "bottomLeftMouseDown" },
+    { kind: "event", event: "topLeftMouseUp" },
+    { kind: "event", event: "topRightMouseUp" },
+    { kind: "event", event: "bottomRightMouseUp" },
+    { kind: "event", event: "bottomLeftMouseUp" },
   ],
 });

src/App/Plant/Dummy/Dummy.tsx

@@ -1,17 +1,18 @@
 import { Plant } from "../Plant";
 import { TimedReactive } from "@/statecharts/timed_reactive";
 
-export const dummyExecution: TimedReactive<null> = {
-  initial: () => [[], null],
+export const dummyExecution: TimedReactive<{}> = {
+  initial: () => [[], {}],
   timeAdvance: () => Infinity,
   intTransition: () => { throw new Error("dummy never makes intTransition"); },
-  extTransition: () => [[], null],
+  extTransition: () => [[], {}],
 };
 
-export const dummyPlant: Plant<null> = {
+export const dummyPlant: Plant<{}, {}> = {
   uiEvents: [],
   inputEvents: [],
   outputEvents: [],
   execution: dummyExecution,
-  render: (props) => <></>,
-}
+  cleanupState: ({}) => ({}),
+  render: ({}) => <></>,
+};

src/App/Plant/Microwave/Microwave.tsx

@@ -13,12 +13,13 @@ import { memo, useEffect } from "react";
 
 import "./Microwave.css";
 import { useAudioContext } from "../../useAudioContext";
-import { comparePlantRenderProps, makeStatechartPlant, PlantRenderProps, StatechartPlantSpec } from "../Plant";
+import { makeStatechartPlant, PlantRenderProps, StatechartPlantSpec } from "../Plant";
 import { detectConnections } from "@/statecharts/detect_connections";
 import { parseStatechart } from "@/statecharts/parser";
 
 import microwaveConcreteSyntax from "./model.json";
 import { ConcreteSyntax } from "@/App/VisualEditor/VisualEditor";
+import { objectsEqual } from "@/util/util";
 
 export const [microwaveAbstractSyntax, microwaveErrors] = parseStatechart(microwaveConcreteSyntax as ConcreteSyntax, detectConnections(microwaveConcreteSyntax as ConcreteSyntax));
 
@@ -27,7 +28,6 @@ if (microwaveErrors.length > 0) {
   throw new Error("there were errors parsing microwave plant model. see console.")
 }
 
-
 const imgs = {
   "false": { "false": imgSmallClosedOff, "true": imgSmallClosedOn },
   "true": { "false": imgSmallOpenedOff, "true": imgSmallOpenedOn },
@@ -47,7 +47,19 @@ const DOOR_Y0 = 68;
 const DOOR_WIDTH = 353;
 const DOOR_HEIGHT = 217;
 
-export const Microwave = memo(function Microwave({state, speed, raiseUIEvent}: PlantRenderProps<RT_Statechart>) {
+type MicrowaveState = {
+  bellRinging: boolean,
+  magnetronRunning: boolean,
+  doorOpen: boolean,
+  timeDisplay: number,
+
+  // these booleans are true for as long as the respective button is pressed (i.e., mouse button is down)
+  startPressed: boolean,
+  stopPressed: boolean,
+  incTimePressed: boolean,
+}
+
+export const Microwave = memo(function Microwave({state: {bellRinging, magnetronRunning, doorOpen, timeDisplay}, speed, raiseUIEvent}: PlantRenderProps<MicrowaveState>) {
   const [playSound, preloadAudio] = useAudioContext(speed);
 
   // preload(imgSmallClosedOff, {as: "image"});
@@ -58,11 +70,6 @@ export const Microwave = memo(function Microwave({state, speed, raiseUIEvent}: P
   preloadAudio(sndRunning);
   preloadAudio(sndBell);
 
-  const bellRinging = state.mode.has("12");
-  const magnetronRunning = state.mode.has("8");
-  const doorOpen = state.mode.has("7");
-  const timeDisplay = state.environment.get("timeDisplay");
-
   // a bit hacky: when the bell-state changes to true, we play the bell sound...
   useEffect(() => {
     if (bellRinging) {
@@ -90,16 +97,16 @@ export const Microwave = memo(function Microwave({state, speed, raiseUIEvent}: P
       <image xlinkHref={imgs[doorOpen][magnetronRunning]} width={520} height={348}/>
 
       <rect className="microwaveButtonHelper" x={START_X0} y={START_Y0} width={BUTTON_WIDTH} height={BUTTON_HEIGHT} 
-        onMouseDown={() => raiseUIEvent({name: "startPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "startReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "startMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "startMouseUp"})}
       />
       <rect className="microwaveButtonHelper" x={STOP_X0} y={STOP_Y0} width={BUTTON_WIDTH} height={BUTTON_HEIGHT} 
-        onMouseDown={() => raiseUIEvent({name: "stopPressed"})}
-        onMouseUp={() => raiseUIEvent({name: "stopReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "stopMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "stopMouseUp"})}
       />
       <rect className="microwaveButtonHelper" x={INCTIME_X0} y={INCTIME_Y0} width={BUTTON_WIDTH} height={BUTTON_HEIGHT} 
-        onMouseDown={() => raiseUIEvent({name: "incTimePressed"})}
-        onMouseUp={() => raiseUIEvent({name: "incTimeReleased"})}
+        onMouseDown={() => raiseUIEvent({name: "incTimeMouseDown"})}
+        onMouseUp={() => raiseUIEvent({name: "incTimeMouseUp"})}
       />
       <rect className="microwaveDoorHelper"
         x={DOOR_X0} y={DOOR_Y0} width={DOOR_WIDTH} height={DOOR_HEIGHT}
@@ -110,20 +117,31 @@ export const Microwave = memo(function Microwave({state, speed, raiseUIEvent}: P
       <text x={472} y={106} textAnchor="end" fontFamily="digital-font" fontSize={24} fill="lightgreen">{timeDisplay}</text>
     </svg>
   </>;
-}, comparePlantRenderProps);
+}, objectsEqual);
 
-const microwavePlantSpec: StatechartPlantSpec = {
+const microwavePlantSpec: StatechartPlantSpec<MicrowaveState> = {
   ast: microwaveAbstractSyntax,
+  cleanupState: (state: RT_Statechart) => {
+    const bellRinging = state.mode.has(microwaveAbstractSyntax.label2State.get("bell")!.uid);
+    const magnetronRunning = state.mode.has(microwaveAbstractSyntax.label2State.get("Magnetron on")!.uid);
+    const doorOpen = state.mode.has(microwaveAbstractSyntax.label2State.get("Door opened")!.uid);
+    const startPressed = state.mode.has(microwaveAbstractSyntax.label2State.get("startPressed")!.uid);
+    const stopPressed = state.mode.has(microwaveAbstractSyntax.label2State.get("stopPressed")!.uid);
+    const incTimePressed = state.mode.has(microwaveAbstractSyntax.label2State.get("incTimePressed")!.uid);
+    // let startPressed, stopPressed, incTimePressed;
+    const timeDisplay = state.environment.get("timeDisplay");
+    return {bellRinging, magnetronRunning, doorOpen, timeDisplay, startPressed, stopPressed, incTimePressed};
+  },
   render: Microwave,
   uiEvents: [
     {kind: "event", event: "doorMouseDown"},
     {kind: "event", event: "doorMouseUp"},
-    {kind: "event", event: "startPressed"},
-    {kind: "event", event: "startReleased"},
-    {kind: "event", event: "stopPressed"},
-    {kind: "event", event: "stopReleased"},
-    {kind: "event", event: "incTimePressed"},
-    {kind: "event", event: "incTimeReleased"},
+    {kind: "event", event: "startMouseDown"},
+    {kind: "event", event: "startMouseUp"},
+    {kind: "event", event: "stopMouseDown"},
+    {kind: "event", event: "stopMouseUp"},
+    {kind: "event", event: "incTimeMouseDown"},
+    {kind: "event", event: "incTimeMouseUp"},
   ],
 }
 

src/App/Plant/Plant.ts

@@ -1,9 +1,9 @@
-import { ReactElement, ReactNode } from "react";
+import { ReactNode } from "react";
 import { Statechart } from "@/statecharts/abstract_syntax";
 import { EventTrigger } from "@/statecharts/label_ast";
 import { BigStep, RaisedEvent, RT_Statechart } from "@/statecharts/runtime_types";
 import { statechartExecution, TimedReactive } from "@/statecharts/timed_reactive";
-import { mapsEqual, setsEqual } from "@/util/util";
+import { setsEqual } from "@/util/util";
 
 export type PlantRenderProps<StateType> = {
   state: StateType,
@@ -11,18 +11,19 @@ export type PlantRenderProps<StateType> = {
   raiseUIEvent: (e: RaisedEvent) => void,
 };
 
-export type Plant<StateType> = {
+export type Plant<StateType, CleanStateType> = {
   uiEvents: EventTrigger[];
 
   inputEvents: EventTrigger[];
   outputEvents: EventTrigger[];
 
   execution: TimedReactive<StateType>;
-  render: (props: PlantRenderProps<StateType>) => ReactNode;
+  cleanupState: (state: StateType) => CleanStateType;
+  render: (props: PlantRenderProps<CleanStateType>) => ReactNode;
 }
 
 // Automatically connect Statechart and Plant inputs/outputs if their event names match.
-export function autoConnect(ast: Statechart, scName: string, plant: Plant<any>, plantName: string) {
+export function autoConnect(ast: Statechart, scName: string, plant: Plant<any, any>, plantName: string) {
   const outputs = {
     [scName]: {},
     [plantName]: {},
@@ -44,7 +45,7 @@ export function autoConnect(ast: Statechart, scName: string, plant: Plant<any>,
   return outputs;
 }
 
-export function exposePlantInputs(plant: Plant<any>, plantName: string, tfm = (s: string) => s) {
+export function exposePlantInputs(plant: Plant<any, any>, plantName: string, tfm = (s: string) => s) {
   const inputs = {};
   for (const i of plant.inputEvents) {
     // @ts-ignore
@@ -53,25 +54,27 @@ export function exposePlantInputs(plant: Plant<any>, plantName: string, tfm = (s
   return inputs
 }
 
-export type StatechartPlantSpec = {
+export type StatechartPlantSpec<CleanStateType> = {
   uiEvents: EventTrigger[],
   ast: Statechart,
-  render: (props: PlantRenderProps<RT_Statechart>) => ReactNode,
+  cleanupState: (rtConfig: RT_Statechart) => CleanStateType,
+  render: (props: PlantRenderProps<CleanStateType>) => ReactNode,
 }
 
-export function makeStatechartPlant({uiEvents, ast, render}: StatechartPlantSpec): Plant<BigStep> {
+export function makeStatechartPlant<CleanStateType>({uiEvents, ast, cleanupState, render}: StatechartPlantSpec<CleanStateType>): Plant<BigStep, CleanStateType> {
   return {
     uiEvents,
     inputEvents: ast.inputEvents,
     outputEvents: [...ast.outputEvents].map(e => ({kind: "event" as const, event: e})),
     execution: statechartExecution(ast),
+    cleanupState,
     render,
   }
 }
 
-export function comparePlantRenderProps(oldProps: PlantRenderProps<RT_Statechart>, newProps: PlantRenderProps<RT_Statechart>) {
-  return setsEqual(oldProps.state.mode, newProps.state.mode)
-    && oldProps.state.environment === newProps.state.environment // <-- could optimize this further
-    && oldProps.speed === newProps.speed
-    && oldProps.raiseUIEvent === newProps.raiseUIEvent
-}
+// export function comparePlantRenderProps(oldProps: PlantRenderProps<RT_Statechart>, newProps: PlantRenderProps<RT_Statechart>) {
+//   return setsEqual(oldProps.state.mode, newProps.state.mode)
+//     && oldProps.state.environment === newProps.state.environment // <-- could optimize this further
+//     && oldProps.speed === newProps.speed
+//     && oldProps.raiseUIEvent === newProps.raiseUIEvent
+// }

src/App/Plant/TrafficLight/TrafficLight.tsx

@@ -11,10 +11,11 @@ import trafficLightConcreteSyntax from "./model.json";
 import { parseStatechart } from "@/statecharts/parser";
 import { ConcreteSyntax } from "@/App/VisualEditor/VisualEditor";
 import { detectConnections } from "@/statecharts/detect_connections";
-import { comparePlantRenderProps, makeStatechartPlant, PlantRenderProps, StatechartPlantSpec } from "../Plant";
+import { makeStatechartPlant, PlantRenderProps, StatechartPlantSpec } from "../Plant";
 import { RT_Statechart } from "@/statecharts/runtime_types";
 import { useAudioContext } from "@/App/useAudioContext";
 import { memo, useEffect } from "react";
+import { objectsEqual } from "@/util/util";
 
 const [trafficLightAbstractSyntax, trafficLightErrors] = parseStatechart(trafficLightConcreteSyntax as ConcreteSyntax, detectConnections(trafficLightConcreteSyntax as ConcreteSyntax));
 
@@ -23,19 +24,20 @@ if (trafficLightErrors.length > 0) {
   throw new Error("there were errors parsing traffic light plant model. see console.")
 }
 
-export const TrafficLight = memo(function TrafficLight({state, speed, raiseUIEvent}: PlantRenderProps<RT_Statechart>) {
+type TrafficLightState = {
+  redOn: boolean,
+  yellowOn: boolean,
+  greenOn: boolean,
+  timerGreen: boolean,
+  timerValue: number,
+}
+
+export const TrafficLight = memo(function TrafficLight({state: {redOn, yellowOn, greenOn, timerGreen, timerValue}, speed, raiseUIEvent}: PlantRenderProps<TrafficLightState>) {
   // preload(imgBackground, {as: "image"});
   preload(imgRedOverlay, {as: "image"});
   preload(imgYellowOverlay, {as: "image"});
   preload(imgGreenOverlay, {as: "image"});
   
-  const redOn = state.mode.has("85");
-  const yellowOn = state.mode.has("87");
-  const greenOn = state.mode.has("89");
-
-  const timerGreen = state.mode.has("137");
-  const timerValue = state.environment.get("t");
-
   const [playURL, preloadAudio] = useAudioContext(speed);
 
   // preloadAudio(sndAtmosphere);
@@ -89,10 +91,20 @@ export const TrafficLight = memo(function TrafficLight({state, speed, raiseUIEve
     <br/>
     <button onClick={() => raiseUIEvent({name: "policeInterrupt"})}>POLICE INTERRUPT</button>
   </>;
-}, comparePlantRenderProps);
+}, (oldProps, newProps) => {
+  return objectsEqual(oldProps, newProps);
+});
 
-const trafficLightPlantSpec: StatechartPlantSpec = {
+const trafficLightPlantSpec: StatechartPlantSpec<TrafficLightState> = {
   ast: trafficLightAbstractSyntax,
+  cleanupState: (state: RT_Statechart) => {
+    const redOn = state.mode.has("85");
+    const yellowOn = state.mode.has("87");
+    const greenOn = state.mode.has("89");
+    const timerGreen = state.mode.has("137");
+    const timerValue = state.environment.get("t");
+    return { redOn, yellowOn, greenOn, timerGreen, timerValue };
+  },
   render: TrafficLight,
   uiEvents: [
     {kind: "event", event: "policeInterrupt"},

src/App/RTHistory.tsx

@@ -12,9 +12,30 @@ type RTHistoryProps = {
   ast: Statechart,
   setTime: Dispatch<SetStateAction<TimeMode>>,
   showPlantTrace: boolean,
+  propertyTrace: {timestamp: number, satisfied: boolean}[] | null,
 }
 
-export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace}: RTHistoryProps) {
+function lookupPropertyStatus(simtime: number, propertyTrace: {timestamp: number, satisfied: boolean}[], startAt=0): [number, boolean | undefined] {
+  let i = startAt;
+  while (i >= 0 && i < propertyTrace.length) {
+    const {timestamp} = propertyTrace[i];
+    if (timestamp === simtime) {
+      // exact match
+      break;
+    }
+    else if (timestamp > simtime) {
+      i--;
+      // too far
+      break;
+    }
+    // continue...
+    i++;
+  }
+  i = Math.min(i, propertyTrace.length-1);
+  return [i, propertyTrace[i] && propertyTrace[i].satisfied];
+}
+
+export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace, propertyTrace}: RTHistoryProps) {
   const onMouseDown = useCallback((idx: number, timestamp: number) => {
     setTrace(trace => trace && {
       ...trace,
@@ -26,6 +47,7 @@ export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace}: RTHis
   if (trace === null) {
     return <></>;
   }
+  let j = 0;
   return trace.trace.map((item, i) => {
     const prevItem = trace.trace[i-1];
     // @ts-ignore
@@ -33,7 +55,16 @@ export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace}: RTHis
     if (!showPlantTrace && isPlantStep) {
       return <></>
     }
-    return <RTHistoryItem ast={ast} idx={i} item={item} prevItem={prevItem} isPlantStep={isPlantStep} active={i === trace.idx} onMouseDown={onMouseDown}/>;
+    let propertyClasses = "status";
+    if (propertyTrace !== null) {
+      let satisfied;
+      [j, satisfied] = lookupPropertyStatus(item.simtime, propertyTrace, j);
+      // console.log(item.simtime, j, propertyTrace[j]);
+      if (satisfied !== null && satisfied !== undefined) {
+        propertyClasses += (satisfied ? " satisfied" : " violated");
+      }
+    }
+    return <RTHistoryItem ast={ast} idx={i} item={item} prevItem={prevItem} isPlantStep={isPlantStep} active={i === trace.idx} onMouseDown={onMouseDown} propertyClasses={propertyClasses} />;
   });
 }
 
@@ -55,7 +86,7 @@ function RTEventParam(props: {param?: any}) {
   return <>{props.param !== undefined && <>({JSON.stringify(props.param)})</>}</>;
 }
 
-export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevItem, isPlantStep, active, onMouseDown}: {idx: number, ast: Statechart, item: TraceItem, prevItem?: TraceItem, isPlantStep: boolean, active: boolean, onMouseDown: (idx: number, timestamp: number) => void}) {
+export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevItem, isPlantStep, active, onMouseDown, propertyClasses}: {idx: number, ast: Statechart, item: TraceItem, prevItem?: TraceItem, isPlantStep: boolean, active: boolean, onMouseDown: (idx: number, timestamp: number) => void, propertyClasses: string}) {
   if (item.kind === "bigstep") {
     // @ts-ignore
     const newStates = item.state.sc.mode.difference(prevItem?.state.sc.mode || new Set());
@@ -63,6 +94,8 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
       className={"runtimeState" + (active ? " active" : "") + (isPlantStep ? " plantStep" : "")}
       onMouseDown={useCallback(() => onMouseDown(idx, item.simtime), [idx, item.simtime])}>
       <div>
+        <div className={propertyClasses}/>
+        &emsp;
         {formatTime(item.simtime)}
         &emsp;
         <div className="inputEvent"><RTCause cause={isPlantStep ? item.state.plant.inputEvent : item.state.sc.inputEvent}/></div>

src/App/ShowAST.tsx

@@ -118,7 +118,7 @@ export function ShowInputEvents({inputEvents, onRaise, disabled, showKeys}: {inp
     const value = inputParams[key] || "";
     const width = Math.max(value.length, (paramName||"").length)*6;
     const shortcut = (i+1)%10;
-    const KI = (i <= 10) ? KeyInfo : KeyInfoHidden;
+    const KI = (i < 10) ? KeyInfo : KeyInfoHidden;
     return <div key={key} className="toolbarGroup">
       <KI keyInfo={<kbd>{shortcut}</kbd>} horizontal={true}>
         <button

src/App/TopPanel/SpeedControl.tsx

@@ -30,6 +30,8 @@ export const SpeedControl = memo(function SpeedControl({showKeys, timescale, set
   }, [onTimeScaleChange, timescale]);
 
   const onKeyDown = useCallback((e: KeyboardEvent) => {
+    // @ts-ignore
+    if (["INPUT", "TEXTAREA", "SELECT"].includes(e.target?.tagName)) return;
     if (!e.ctrlKey) {
       if (e.key === "s") {
         e.preventDefault();

src/App/VisualEditor/useCopyPaste.ts

@@ -118,6 +118,8 @@ export function useCopyPaste(makeCheckPoint: () => void, state: VisualEditorStat
   }, [setState]);
 
   const onKeyDown = (e: KeyboardEvent) => {
+    // @ts-ignore
+    if (["INPUT", "TEXTAREA", "SELECT"].includes(e.target?.tagName)) return;
     if (e.key === "Delete") {
       // delete selection
       makeCheckPoint();

src/App/check_property.ts

@@ -0,0 +1,79 @@
+import { RT_Statechart } from "@/statecharts/runtime_types";
+import { TraceItem } from "./App";
+import { Plant } from "./Plant/Plant";
+
+// const endpoint = "http://localhost:15478/check_property";
+const endpoint = "https://deemz.org/apis/mtl-aas/check_property";
+
+export type PropertyTrace = {
+  timestamp: number,
+  satisfied: boolean,
+}[];
+
+export type PropertyCheckResult = [null|PropertyTrace, null|string];
+
+export async function checkProperty(plant: Plant<RT_Statechart, any>, property: string, trace: [TraceItem, ...TraceItem[]]): Promise<PropertyCheckResult> {
+  // pre-process data...
+
+  const cleanPlantStates0 = trace
+    .map(v => {
+      return {
+        simtime: v.simtime,
+        state: Object.fromEntries(Object.entries(v.kind === "bigstep" && plant.cleanupState(v.state.plant) || {}).map(([prop, val]) => [prop, Boolean(val)])),
+      };
+    });
+
+  const cleanPlantStates = cleanPlantStates0 && cleanPlantStates0
+    // we can never have multiple states at the same point in simtime or Argus will panic
+    .reduce((trace, entry, i) => {
+      const prevEntry = cleanPlantStates0[i-1];
+      if (prevEntry !== undefined) {
+        if (entry.simtime > prevEntry.simtime) {
+          return [...trace, entry]; // ok
+        }
+        return [...trace.slice(0,-1), entry]; // current entry has same simtime and thus replaces previous entry
+      }
+      return [entry];
+    }, [] as {simtime: number, state: any}[]);
+
+  let traces = {} as {[key: string]: [number, any][]};
+  for (const {simtime, state} of cleanPlantStates) {
+    for (const [key, value] of Object.entries(state)) {
+      // just append
+      traces[key] = traces[key] || [];
+      const prevSample = traces[key].at(-1);
+      // only append sample if value changed:
+      if (!prevSample || prevSample[1] !== value) {
+        traces[key].push([simtime, value]);
+      }
+    }
+  }
+
+  console.log({cleanPlantStates, traces});
+
+  try {
+    const response = await fetch(endpoint, {
+      method: "POST",
+      headers: {
+        "Content-Type": "application/json",
+      },
+      body: JSON.stringify({
+        property,
+        traces,
+      }),
+    });
+
+    const json = await response.json();
+    // console.log('backend result:', json);
+
+    if (typeof json === 'string') {
+      return [null, json];
+    }
+    else {
+      return [json.map(([timestamp, satisfied]) => ({timestamp, satisfied})), null];
+    }
+  }
+  catch (e) {
+    return [null, e.message];
+  }
+}

src/App/useEditor.ts

@@ -7,9 +7,9 @@ import { emptyState } from "@/statecharts/concrete_syntax";
 
 export function useEditor(editorState: VisualEditorState | null, setEditHistory: Dispatch<SetStateAction<EditHistory|null>>) {
   useEffect(() => {
-    console.log("Welcome to StateBuddy!");
+    console.info("Welcome to StateBuddy!");
     () => {
-      console.log("Goodbye!");
+      console.info("Goodbye!");
     }
   }, []);