From 49e701c7d7e77a200d5635cb27056eabc4b63691 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Thu, 6 Nov 2025 18:48:37 +0100 Subject: [PATCH 1/2] nearly the entire application state is saved in URL --- src/App/App.css | 2 + src/App/App.tsx | 159 ++++++++++++++++++++++++------- src/App/RTHistory.tsx | 30 ++++-- src/App/ShowAST.tsx | 25 +---- src/App/check_property.ts | 2 + src/App/useEditor.ts | 61 +----------- src/App/useUrlHashState.ts | 185 +++++++++++++++++++++++++++++++++++++ 7 files changed, 338 insertions(+), 126 deletions(-) create mode 100644 src/App/useUrlHashState.ts diff --git a/src/App/App.css b/src/App/App.css index d15f623..76f1272 100644 --- a/src/App/App.css +++ b/src/App/App.css @@ -129,6 +129,8 @@ div.status { border-radius: 50%; height: 12px; width: 12px; + margin-left: 4px; + margin-right: 4px; } div.status.violated { diff --git a/src/App/App.tsx b/src/App/App.tsx index e5a4a8c..68f7bc5 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -7,6 +7,8 @@ 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 SaveOutlinedIcon from '@mui/icons-material/SaveOutlined'; +import CachedOutlinedIcon from '@mui/icons-material/CachedOutlined'; import { Statechart } from "@/statecharts/abstract_syntax"; import { detectConnections } from "@/statecharts/detect_connections"; @@ -30,6 +32,7 @@ import { VisualEditor, VisualEditorState } from "./VisualEditor/VisualEditor"; import { checkProperty, PropertyCheckResult } from "./check_property"; import { usePersistentState } from "./persistent_state"; import { useEditor } from "./useEditor"; +import { useUrlHashState } from "./useUrlHashState"; export type EditHistory = { current: VisualEditorState, @@ -47,7 +50,7 @@ const plants: [string, Plant][] = [ ] export type TraceItemError = { - cause: string, // event name, or + cause: BigStepCause, // event name, or simtime: number, error: RuntimeError, } @@ -58,9 +61,21 @@ type CoupledState = { // plantCleanState: {[prop: string]: boolean|number}, }; +export type BigStepCause = { + kind: "init", +} | { + kind: "input", + simtime: number, + eventName: string, + param?: any, +} | { + kind: "timer", + simtime: number, +}; + export type TraceItem = { kind: "error" } & TraceItemError -| { kind: "bigstep", simtime: number, cause: string, state: CoupledState, outputEvents: RaisedEvent[] }; +| { kind: "bigstep", simtime: number, cause: BigStepCause, state: CoupledState, outputEvents: RaisedEvent[] }; export type TraceState = { trace: [TraceItem, ...TraceItem[]], // non-empty @@ -68,27 +83,46 @@ export type TraceState = { }; export function App() { - const [insertMode, setInsertMode] = usePersistentState("insertMode", "and"); const [editHistory, setEditHistory] = useState(null); const [trace, setTrace] = useState(null); const [time, setTime] = useState({kind: "paused", simtime: 0}); const [modal, setModal] = useState(null); - const [plantName, setPlantName] = usePersistentState("plant", "dummy"); - const [zoom, setZoom] = usePersistentState("zoom", 1); - const [showKeys, setShowKeys] = usePersistentState("shortcuts", true); - - const [autoScroll, setAutoScroll] = usePersistentState("autoScroll", true); - const [autoConnect, setAutoConnect] = usePersistentState("autoConnect", true); - const [plantConns, setPlantConns] = usePersistentState("plantConns", {}); - - const plant = plants.find(([pn, p]) => pn === plantName)![1]; + const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(setEditHistory); const editorState = editHistory && editHistory.current; const setEditorState = useCallback((cb: (value: VisualEditorState) => VisualEditorState) => { setEditHistory(historyState => historyState && ({...historyState, current: cb(historyState.current)})); }, [setEditHistory]); + const { + autoConnect, + setAutoConnect, + autoScroll, + setAutoScroll, + plantConns, + setPlantConns, + showKeys, + setShowKeys, + zoom, + setZoom, + insertMode, + setInsertMode, + plantName, + setPlantName, + showExecutionTrace, + setShowExecutionTrace, + showPlantTrace, + setShowPlantTrace, + properties, + setProperties, + savedTraces, + setSavedTraces, + activeProperty, + setActiveProperty, + } = useUrlHashState(editorState, setEditHistory); + const plant = plants.find(([pn, p]) => pn === plantName)![1]; + const refRightSideBar = useRef(null); // parse concrete syntax always: @@ -105,8 +139,6 @@ export function App() { }] : [], ]; - const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(editorState, setEditHistory); - const scrollDownSidebar = useCallback(() => { if (autoScroll && refRightSideBar.current) { const el = refRightSideBar.current; @@ -128,7 +160,7 @@ export function App() { const onInit = useCallback(() => { if (cE === null) return; - const metadata = {simtime: 0, cause: ""}; + const metadata = {simtime: 0, cause: {kind: "init" as const}}; try { const [outputEvents, state] = cE.initial(); // may throw if initialing the statechart results in a RuntimeError setTrace({ @@ -169,7 +201,7 @@ export function App() { if (currentTraceItem !== null /*&& ast.inputEvents.some(e => e.event === inputEvent)*/) { if (currentTraceItem.kind === "bigstep") { const simtime = getSimTime(time, Math.round(performance.now())); - appendNewConfig(simtime, inputEvent, () => { + appendNewConfig(simtime, {kind: "input", simtime, eventName: inputEvent, param}, () => { return cE.extTransition(simtime, currentTraceItem.state, {kind: "input", name: inputEvent, param}); }); } @@ -184,7 +216,7 @@ export function App() { const nextTimeout = cE?.timeAdvance(currentTraceItem.state); const raiseTimeEvent = () => { - appendNewConfig(nextTimeout, "", () => { + appendNewConfig(nextTimeout, {kind: "timer", simtime: nextTimeout}, () => { return cE.intTransition(currentTraceItem.state); }); } @@ -207,7 +239,7 @@ export function App() { } }, [time, currentTraceItem]); // <-- todo: is this really efficient? - function appendNewConfig(simtime: number, cause: string, computeNewState: () => [RaisedEvent[], CoupledState]) { + function appendNewConfig(simtime: number, cause: BigStepCause, computeNewState: () => [RaisedEvent[], CoupledState]) { let newItem: TraceItem; const metadata = {simtime, cause} try { @@ -258,8 +290,6 @@ export function App() { const highlightActive = (currentBigStep && currentBigStep.state.sc.mode) || new Set(); const highlightTransitions = currentBigStep && currentBigStep.state.sc.firedTransitions || []; - const [showExecutionTrace, setShowExecutionTrace] = usePersistentState("showExecutionTrace", true); - const [showPlantTrace, setShowPlantTrace] = usePersistentState("showPlantTrace", false); const speed = time.kind === "paused" ? 0 : time.scale; @@ -269,9 +299,53 @@ export function App() { ast && autoConnect && autoDetectConns(ast, plant, setPlantConns); }, [ast, plant, autoConnect]); - const [properties, setProperties] = usePersistentState("properties", []); const [propertyResults, setPropertyResults] = useState(null); - const [activeProperty, setActiveProperty] = usePersistentState("activeProperty", 0); + + + const onSaveTrace = () => { + if (trace) { + setSavedTraces(savedTraces => [ + ...savedTraces, + ["untitled", trace.trace.map((item) => item.cause)] as [string, BigStepCause[]], + ]); + } + } + + const onReplayTrace = (causes: BigStepCause[]) => { + if (cE) { + function run_until(simtime: number) { + while (true) { + const nextTimeout = cE!.timeAdvance(lastState); + if (nextTimeout > simtime) { + break; + } + const [outputEvents, coupledState] = cE!.intTransition(lastState); + lastState = coupledState; + lastSimtime = nextTimeout; + newTrace.push({kind: "bigstep", simtime: nextTimeout, state: coupledState, outputEvents, cause: {kind: "timer", simtime: nextTimeout}}); + } + } + const [outputEvents, coupledState] = cE.initial(); + const newTrace = [{kind: "bigstep", simtime: 0, state: coupledState, outputEvents, cause: {kind: "init"} as BigStepCause} as TraceItem] as [TraceItem, ...TraceItem[]]; + let lastState = coupledState; + let lastSimtime = 0; + for (const cause of causes) { + if (cause.kind === "input") { + run_until(cause.simtime); // <-- just make sure we haven't missed any timers elapsing + // @ts-ignore + const [outputEvents, coupledState] = cE.extTransition(cause.simtime, newTrace.at(-1)!.state, {kind: "input", name: cause.eventName, param: cause.param}); + lastState = coupledState; + lastSimtime = cause.simtime; + newTrace.push({kind: "bigstep", simtime: cause.simtime, state: coupledState, outputEvents, cause}); + } + else if (cause.kind === "timer") { + run_until(cause.simtime); + } + } + setTrace({trace: newTrace, idx: newTrace.length-1}); + setTime({kind: "paused", simtime: lastSimtime}); + } + } // if some properties change, re-evaluate them: useEffect(() => { @@ -395,11 +469,6 @@ export function App() { {/* Properties */} properties -
- -
{properties.map((property, i) => { const result = propertyResults && propertyResults[i]; let violated = null, propertyError = null; @@ -409,25 +478,47 @@ export function App() { } return
-   - setProperties(properties => properties.toSpliced(i, 1, e.target.value))}/> + setProperties(properties => properties.toSpliced(i, 1, e.target.value))}/> {propertyError &&
{propertyError}
}
; })} +
+ +
{/* Traces */} -
setShowExecutionTrace(e.newState === "open")}>execution trace - setShowPlantTrace(e.target.checked)}/> - - setAutoScroll(e.target.checked)}/> - +
+ {savedTraces.map((savedTrace, i) => +
+ + setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1, [e.target.value, savedTraces[i][1]]))}/> + +
+ )} +
+
+ setShowPlantTrace(e.target.checked)}/> + + setAutoScroll(e.target.checked)}/> + +   + +
diff --git a/src/App/RTHistory.tsx b/src/App/RTHistory.tsx index acce59c..d834399 100644 --- a/src/App/RTHistory.tsx +++ b/src/App/RTHistory.tsx @@ -3,7 +3,7 @@ import { Statechart, stateDescription } from "../statecharts/abstract_syntax"; import { Mode, RaisedEvent, RT_Event } from "../statecharts/runtime_types"; import { formatTime } from "../util/util"; import { TimeMode, timeTravel } from "../statecharts/time"; -import { TraceItem, TraceState } from "./App"; +import { BigStepCause, TraceItem, TraceState } from "./App"; import { Environment } from "@/statecharts/environment"; type RTHistoryProps = { @@ -15,6 +15,8 @@ type RTHistoryProps = { propertyTrace: {timestamp: number, satisfied: boolean}[] | null, } +type PropertyStatus = "unknown" | "satisfied" | "violated"; + function lookupPropertyStatus(simtime: number, propertyTrace: {timestamp: number, satisfied: boolean}[], startAt=0): [number, boolean | undefined] { let i = startAt; while (i >= 0 && i < propertyTrace.length) { @@ -55,16 +57,16 @@ export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace, proper if (!showPlantTrace && isPlantStep) { return <> } - let propertyClasses = "status"; + let propertyStatus: PropertyStatus = "unknown"; 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"); + propertyStatus = (satisfied ? "satisfied" : "violated"); } } - return ; + return ; }); } @@ -78,7 +80,7 @@ function RTCause(props: {cause?: RT_Event}) { else if (props.cause.kind === "input") { return <>{props.cause.name} } - console.log(props.cause); + // console.log(props.cause); throw new Error("unreachable"); } @@ -86,7 +88,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, propertyClasses}: {idx: number, ast: Statechart, item: TraceItem, prevItem?: TraceItem, isPlantStep: boolean, active: boolean, onMouseDown: (idx: number, timestamp: number) => void, propertyClasses: string}) { +export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevItem, isPlantStep, active, onMouseDown, propertyStatus}: {idx: number, ast: Statechart, item: TraceItem, prevItem?: TraceItem, isPlantStep: boolean, active: boolean, onMouseDown: (idx: number, timestamp: number) => void, propertyStatus: PropertyStatus}) { if (item.kind === "bigstep") { // @ts-ignore const newStates = item.state.sc.mode.difference(prevItem?.state.sc.mode || new Set()); @@ -94,7 +96,7 @@ 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])}>
-
+
  {formatTime(item.simtime)}   @@ -115,7 +117,7 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
{formatTime(item.simtime)}   -
{item.cause}
+
{item.error.message} @@ -124,6 +126,18 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt } }); +function ShowCause(props: {cause: BigStepCause}) { + if (props.cause.kind === "init") { + return {""}; + } + else if (props.cause.kind === "timer") { + return {""}; + } + else { + return {props.cause.eventName}; + } +} + function ShowEnvironment(props: {environment: Environment}) { return
{ diff --git a/src/App/ShowAST.tsx b/src/App/ShowAST.tsx index 3354c0f..8657331 100644 --- a/src/App/ShowAST.tsx +++ b/src/App/ShowAST.tsx @@ -44,30 +44,6 @@ export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | Unst } ; - - // return
- // {props.root.kind}: {description} - - // {/* {props.root.kind !== "pseudo" && props.root.entryActions.length>0 && - // props.root.entryActions.map(action => - //
 entry /
- // ) - // } - // {props.root.kind !== "pseudo" && props.root.exitActions.length>0 && - // props.root.exitActions.map(action => - //
 exit /
- // ) - // } */} - - // {props.root.kind !== "pseudo" && props.root.children.length>0 && - // props.root.children.map(child => - // - // ) - // } - // {/* {outgoing.length>0 && - // outgoing.map(transition => <> 
) - // } */} - //
; }); import BoltIcon from '@mui/icons-material/Bolt'; @@ -95,6 +71,7 @@ export function ShowInputEvents({inputEvents, onRaise, disabled, showKeys}: {inp }); const onKeyDown = (e: KeyboardEvent) => { // don't capture keyboard events when focused on an input element: + // @ts-ignore if (["INPUT", "TEXTAREA", "SELECT"].includes(e.target?.tagName)) return; const n = (parseInt(e.key)+9) % 10; diff --git a/src/App/check_property.ts b/src/App/check_property.ts index 9b571d2..ff6e25a 100644 --- a/src/App/check_property.ts +++ b/src/App/check_property.ts @@ -70,10 +70,12 @@ export async function checkProperty(plant: Plant, property: return [null, json]; } else { + // @ts-ignore return [json.map(([timestamp, satisfied]) => ({timestamp, satisfied})), null]; } } catch (e) { + // @ts-ignore return [null, e.message]; } } \ No newline at end of file diff --git a/src/App/useEditor.ts b/src/App/useEditor.ts index 8ca0f52..e1ca293 100644 --- a/src/App/useEditor.ts +++ b/src/App/useEditor.ts @@ -3,9 +3,8 @@ import { HISTORY_RADIUS } from "./parameters"; import { Dispatch, SetStateAction, useCallback, useEffect } from "react"; import { EditHistory } from "./App"; import { VisualEditorState } from "./VisualEditor/VisualEditor"; -import { emptyState } from "@/statecharts/concrete_syntax"; -export function useEditor(editorState: VisualEditorState | null, setEditHistory: Dispatch>) { +export function useEditor(setEditHistory: Dispatch>) { useEffect(() => { console.info("Welcome to StateBuddy!"); () => { @@ -13,64 +12,6 @@ export function useEditor(editorState: VisualEditorState | null, setEditHistory: } }, []); - // recover editor state from URL - we need an effect here because decompression is asynchronous - useEffect(() => { - console.log('recovering state...'); - const compressedState = window.location.hash.slice(1); - if (compressedState.length === 0) { - // empty URL hash - console.log("no state to recover"); - setEditHistory(() => ({current: emptyState, history: [], future: []})); - return; - } - let compressedBuffer; - try { - compressedBuffer = Uint8Array.fromBase64(compressedState); // may throw - } catch (e) { - // probably invalid base64 - console.error("failed to recover state:", e); - setEditHistory(() => ({current: emptyState, history: [], future: []})); - return; - } - const ds = new DecompressionStream("deflate"); - const writer = ds.writable.getWriter(); - writer.write(compressedBuffer).catch(() => {}); // any promise rejections will be detected when we try to read - writer.close().catch(() => {}); - new Response(ds.readable).arrayBuffer() - .then(decompressedBuffer => { - const recoveredState = JSON.parse(new TextDecoder().decode(decompressedBuffer)); - setEditHistory(() => ({current: recoveredState, history: [], future: []})); - }) - .catch(e => { - // any other error: invalid JSON, or decompression failed. - console.error("failed to recover state:", e); - setEditHistory({current: emptyState, history: [], future: []}); - }); - }, []); - - // save editor state in URL - useEffect(() => { - const timeout = setTimeout(() => { - if (editorState === null) { - window.location.hash = "#"; - return; - } - const serializedState = JSON.stringify(editorState); - const stateBuffer = new TextEncoder().encode(serializedState); - const cs = new CompressionStream("deflate"); - const writer = cs.writable.getWriter(); - writer.write(stateBuffer); - writer.close(); - // todo: cancel this promise handler when concurrently starting another compression job - new Response(cs.readable).arrayBuffer().then(compressedStateBuffer => { - const compressedStateString = new Uint8Array(compressedStateBuffer).toBase64(); - window.location.hash = "#"+compressedStateString; - }); - }, 100); - return () => clearTimeout(timeout); - }, [editorState]); - - // append editor state to undo history const makeCheckPoint = useCallback(() => { setEditHistory(historyState => historyState && ({ diff --git a/src/App/useUrlHashState.ts b/src/App/useUrlHashState.ts new file mode 100644 index 0000000..d00a629 --- /dev/null +++ b/src/App/useUrlHashState.ts @@ -0,0 +1,185 @@ +import { Dispatch, SetStateAction, useEffect, useState } from "react"; +import { BigStepCause, EditHistory } from "./App"; +import { VisualEditorState } from "./VisualEditor/VisualEditor"; +import { emptyState } from "@/statecharts/concrete_syntax"; +import { InsertMode } from "./TopPanel/InsertModes"; +import { Conns } from "@/statecharts/timed_reactive"; + +export function useUrlHashState(editorState: VisualEditorState | null, setEditHistory: Dispatch>) { + + // i should probably put all these things into a single object, the 'app state'... + const [autoScroll, setAutoScroll] = useState(true); + const [autoConnect, setAutoConnect] = useState(true); + const [plantConns, setPlantConns] = useState({}); + const [showKeys, setShowKeys] = useState(true); + const [zoom, setZoom] = useState(1); + const [insertMode, setInsertMode] = useState("and"); + const [plantName, setPlantName] = useState("dummy"); + + const [showExecutionTrace, setShowExecutionTrace] = useState(true); + const [showPlantTrace, setShowPlantTrace] = useState(false); + const [properties, setProperties] = useState([]); + const [savedTraces, setSavedTraces] = useState<[string, BigStepCause[]][]>([]); + const [activeProperty, setActiveProperty] = useState(0); + + + // recover editor state from URL - we need an effect here because decompression is asynchronous + useEffect(() => { + console.log('recovering state...'); + const compressedState = window.location.hash.slice(1); + if (compressedState.length === 0) { + // empty URL hash + console.log("no state to recover"); + setEditHistory(() => ({current: emptyState, history: [], future: []})); + return; + } + let compressedBuffer; + try { + compressedBuffer = Uint8Array.fromBase64(compressedState); // may throw + } catch (e) { + // probably invalid base64 + console.error("failed to recover state:", e); + setEditHistory(() => ({current: emptyState, history: [], future: []})); + return; + } + const ds = new DecompressionStream("deflate"); + const writer = ds.writable.getWriter(); + writer.write(compressedBuffer).catch(() => {}); // any promise rejections will be detected when we try to read + writer.close().catch(() => {}); + new Response(ds.readable).arrayBuffer() + .then(decompressedBuffer => { + const recoveredState = JSON.parse(new TextDecoder().decode(decompressedBuffer)); + // we support two formats + if (recoveredState.nextID) { + // old format + setEditHistory(() => ({current: recoveredState, history: [], future: []})); + } + else { + console.log(recoveredState); + // new format + if (recoveredState.editorState !== undefined) { + setEditHistory(() => ({current: recoveredState.editorState, history: [], future: []})); + } + if (recoveredState.plantName !== undefined) { + setPlantName(recoveredState.plantName); + } + if (recoveredState.autoScroll !== undefined) { + setAutoScroll(recoveredState.autoScroll); + } + if (recoveredState.autoConnect !== undefined) { + setAutoConnect(recoveredState.autoConnect); + } + if (recoveredState.plantConns !== undefined) { + setPlantConns(recoveredState.plantConns); + } + + if (recoveredState.showKeys !== undefined) { + setShowKeys(recoveredState.showKeys); + } + if (recoveredState.zoom !== undefined) { + setZoom(recoveredState.zoom); + } + if (recoveredState.insertMode !== undefined) { + setInsertMode(recoveredState.insertMode); + } + if (recoveredState.showExecutionTrace !== undefined) { + setShowExecutionTrace(recoveredState.showExecutionTrace); + } + if (recoveredState.showPlantTrace !== undefined) { + setShowPlantTrace(recoveredState.showPlantTrace); + } + if (recoveredState.properties !== undefined) { + setProperties(recoveredState.properties); + } + if (recoveredState.savedTraces !== undefined) { + setSavedTraces(recoveredState.savedTraces); + } + if (recoveredState.activeProperty !== undefined) { + setActiveProperty(recoveredState.activeProperty); + } + + } + }) + .catch(e => { + // any other error: invalid JSON, or decompression failed. + console.error("failed to recover state:", e); + setEditHistory({current: emptyState, history: [], future: []}); + }); + }, []); + + // save editor state in URL + useEffect(() => { + const timeout = setTimeout(() => { + if (editorState === null) { + window.location.hash = "#"; + return; + } + const serializedState = JSON.stringify({ + autoConnect, + autoScroll, + plantConns, + showKeys, + zoom, + insertMode, + plantName, + editorState, + showExecutionTrace, + showPlantTrace, + properties, + savedTraces, + activeProperty, + }); + const stateBuffer = new TextEncoder().encode(serializedState); + const cs = new CompressionStream("deflate"); + const writer = cs.writable.getWriter(); + writer.write(stateBuffer); + writer.close(); + // todo: cancel this promise handler when concurrently starting another compression job + new Response(cs.readable).arrayBuffer().then(compressedStateBuffer => { + const compressedStateString = new Uint8Array(compressedStateBuffer).toBase64(); + window.location.hash = "#"+compressedStateString; + }); + }, 100); + return () => clearTimeout(timeout); + }, [ + autoConnect, + autoScroll, + plantConns, + showKeys, + zoom, + insertMode, + plantName, + showExecutionTrace, + showPlantTrace, + properties, + savedTraces, + activeProperty, + ]); + + return { + autoConnect, + setAutoConnect, + autoScroll, + setAutoScroll, + plantConns, + setPlantConns, + showKeys, + setShowKeys, + zoom, + setZoom, + insertMode, + setInsertMode, + plantName, + setPlantName, + showExecutionTrace, + setShowExecutionTrace, + showPlantTrace, + setShowPlantTrace, + properties, + setProperties, + savedTraces, + setSavedTraces, + activeProperty, + setActiveProperty, + } +} \ No newline at end of file From 3c302a83c59da20d7b53db9311e4b5fc726db3b3 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Thu, 6 Nov 2025 19:12:02 +0100 Subject: [PATCH 2/2] fix bug + more info on stored traces --- src/App/App.tsx | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/App/App.tsx b/src/App/App.tsx index 68f7bc5..e32ea12 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -33,6 +33,7 @@ import { checkProperty, PropertyCheckResult } from "./check_property"; import { usePersistentState } from "./persistent_state"; import { useEditor } from "./useEditor"; import { useUrlHashState } from "./useUrlHashState"; +import { formatTime } from "@/util/util"; export type EditHistory = { current: VisualEditorState, @@ -473,7 +474,7 @@ export function App() { const result = propertyResults && propertyResults[i]; let violated = null, propertyError = null; if (result) { - violated = result[0] && !result[0][0].satisfied; + violated = result[0] && result[0].length > 0 && !result[0][0].satisfied; propertyError = result[1]; } return
@@ -502,7 +503,11 @@ export function App() { - setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1, [e.target.value, savedTraces[i][1]]))}/> +   + {(Math.floor(savedTrace[1].at(-1).simtime/1000))}s + ({savedTrace[1].length}) +   + setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1, [e.target.value, savedTraces[i][1]]))}/>