fix bug + more info on stored traces

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 {

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,8 @@ 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";
+import { formatTime } from "@/util/util";
 
 export type EditHistory = {
   current: VisualEditorState,
@@ -47,7 +51,7 @@ const plants: [string, Plant<any, UniversalPlantState>][] = [
 ]
 
 export type TraceItemError = {
-  cause: string, // event name, <init> or <timer>
+  cause: BigStepCause, // event name, <init> or <timer>
   simtime: number,
   error: RuntimeError,
 }
@@ -58,9 +62,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 +84,46 @@ export type TraceState = {
 };
 
 export function App() {
-  const [insertMode, setInsertMode] = usePersistentState<InsertMode>("insertMode", "and");
   const [editHistory, setEditHistory] = useState<EditHistory|null>(null);
   const [trace, setTrace] = useState<TraceState|null>(null);
   const [time, setTime] = useState<TimeMode>({kind: "paused", simtime: 0});
   const [modal, setModal] = useState<ReactElement|null>(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<Conns>("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<HTMLDivElement>(null);
 
   // parse concrete syntax always:
@@ -105,8 +140,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 +161,7 @@ export function App() {
 
   const onInit = useCallback(() => {
     if (cE === null) return;
-    const metadata = {simtime: 0, cause: "<init>"};
+    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 +202,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 +217,7 @@ export function App() {
         const nextTimeout = cE?.timeAdvance(currentTraceItem.state);
 
         const raiseTimeEvent = () => {
-          appendNewConfig(nextTimeout, "<timer>", () => {
+          appendNewConfig(nextTimeout, {kind: "timer", simtime: nextTimeout}, () => {
             return cE.intTransition(currentTraceItem.state);
           });
         }
@@ -207,7 +240,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 +291,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 +300,53 @@ 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);
+
+
+  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,39 +470,60 @@ export function App() {
             {/* Properties */}
             <PersistentDetails localStorageKey="showProperty" initiallyOpen={false}>
               <summary>properties</summary>
-              <div className="toolbar">
-                <button title="add property" onClick={() => setProperties(properties => [...properties, ""])}>
-                  <AddIcon fontSize="small"/>
-                </button>
-              </div>
               {properties.map((property, i) => {
                 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 <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))}/>
+                  <input type="text" style={{width:'calc(100% - 90px)'}} 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>;
               })}
+              <div className="toolbar">
+                <button title="add property" onClick={() => setProperties(properties => [...properties, ""])}>
+                  <AddIcon fontSize="small"/> add property
+                </button>
+              </div>
             </PersistentDetails>
             {/* Traces */}
-
             <details open={showExecutionTrace} onToggle={e => setShowExecutionTrace(e.newState === "open")}><summary>execution trace</summary>
+              <div>
+                {savedTraces.map((savedTrace, i) =>
+                  <div key={i} className="toolbar">
+                    <button title="replay trace (may give a different result if you changed your model since recording the trace because only input and timer events are recorded)" onClick={() => onReplayTrace(savedTrace[1])}>
+                      <CachedOutlinedIcon fontSize="small"/>
+                    </button>
+                    &nbsp;
+                    <span style={{display:'inline-block', width: 26, fontSize: 9}}>{(Math.floor(savedTrace[1].at(-1).simtime/1000))}s</span>
+                    <span style={{display:'inline-block', width: 22, fontSize: 9}}>({savedTrace[1].length})</span>
+                    &nbsp;
+                    <input title="name of the trace (only for humans - names don't have to be unique or anything)" type="text" value={savedTrace[0]} style={{width: 'calc(100% - 124px)'}} onChange={e => setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1, [e.target.value, savedTraces[i][1]]))}/>
+                    <button title="forget trace" onClick={() => setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1))}>
+                      <DeleteOutlineIcon fontSize="small"/>
+                    </button>
+                  </div>
+                )}
+              </div>
+              <div className="toolbar">
                 <input id="checkbox-show-plant-items" type="checkbox" checked={showPlantTrace} onChange={e => setShowPlantTrace(e.target.checked)}/>
                 <label htmlFor="checkbox-show-plant-items">show plant steps</label>
                 <input id="checkbox-autoscroll" type="checkbox" checked={autoScroll} onChange={e => setAutoScroll(e.target.checked)}/>
                 <label htmlFor="checkbox-autoscroll">auto-scroll</label>
+                &emsp;
+                <button title="save current trace" disabled={trace === null} onClick={() => onSaveTrace()}>
+                  <SaveOutlinedIcon fontSize="small"/> save trace
+                </button>
+              </div>
             </details>
           </div>
 

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 <RTHistoryItem ast={ast} idx={i} item={item} prevItem={prevItem} isPlantStep={isPlantStep} active={i === trace.idx} onMouseDown={onMouseDown} propertyClasses={propertyClasses} />;
+    return <RTHistoryItem ast={ast} idx={i} item={item} prevItem={prevItem} isPlantStep={isPlantStep} active={i === trace.idx} onMouseDown={onMouseDown} propertyStatus={propertyStatus} />;
   });
 }
 
@@ -78,7 +80,7 @@ function RTCause(props: {cause?: RT_Event}) {
   else if (props.cause.kind === "input") {
     return <>{props.cause.name}<RTEventParam param={props.cause.param}/></>
   }
-  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])}>
       <div>
-        <div className={propertyClasses}/>
+        <div className={"status " + propertyStatus}/>
         &emsp;
         {formatTime(item.simtime)}
         &emsp;
@@ -115,7 +117,7 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
       <div>
         {formatTime(item.simtime)}
         &emsp;
-        <div className="inputEvent">{item.cause}</div>
+        <div className="inputEvent"><ShowCause cause={item.cause}/></div>
       </div>
       <div>
         {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 <span>{"<init>"}</span>;
+  }
+  else if (props.cause.kind === "timer") {
+    return <span>{"<timer>"}</span>;
+  }
+  else {
+    return <span>{props.cause.eventName}<RTEventParam param={props.cause.param}/></span>;
+  }
+}
+
 
 function ShowEnvironment(props: {environment: Environment}) {
   return <div>{

src/App/ShowAST.tsx

@@ -44,30 +44,6 @@ export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | Unst
       </ul>
     }
   </li>;
-
-  // return <details open={true} className={"stateTree" + (props.highlightActive.has(props.root.uid) ? " active" : "")}>
-  //   <summary>{props.root.kind}: {description}</summary>
-
-  //   {/* {props.root.kind !== "pseudo" && props.root.entryActions.length>0 &&
-  //       props.root.entryActions.map(action =>
-  //         <div>&emsp;entry / <ShowAction action={action}/></div>
-  //       )
-  //   }
-  //   {props.root.kind !== "pseudo" && props.root.exitActions.length>0 &&
-  //       props.root.exitActions.map(action =>
-  //         <div>&emsp;exit / <ShowAction action={action}/></div>
-  //       )
-  //   } */}
-
-  //   {props.root.kind !== "pseudo" && props.root.children.length>0 &&
-  //         props.root.children.map(child => 
-  //           <ShowAST key={child.uid} root={child} transitions={props.transitions} rt={props.rt} highlightActive={props.highlightActive} />
-  //         )
-  //   }
-  //   {/* {outgoing.length>0 &&
-  //       outgoing.map(transition => <>&emsp;<ShowTransition transition={transition}/><br/></>)
-  //   } */}
-  // </details>;
 });
 
 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;

src/App/check_property.ts

@@ -70,10 +70,12 @@ export async function checkProperty(plant: Plant<RT_Statechart, any>, property:
       return [null, json];
     }
     else {
+      // @ts-ignore
       return [json.map(([timestamp, satisfied]) => ({timestamp, satisfied})), null];
     }
   }
   catch (e) {
+    // @ts-ignore
     return [null, e.message];
   }
 }

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<SetStateAction<EditHistory|null>>) {
+export function useEditor(setEditHistory: Dispatch<SetStateAction<EditHistory|null>>) {
   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 && ({

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<SetStateAction<EditHistory|null>>) {
+
+  // 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<Conns>({});
+  const [showKeys, setShowKeys] = useState(true);
+  const [zoom, setZoom] = useState(1);
+  const [insertMode, setInsertMode] = useState<InsertMode>("and");
+  const [plantName, setPlantName] = useState("dummy");
+
+  const [showExecutionTrace, setShowExecutionTrace] = useState(true);
+  const [showPlantTrace, setShowPlantTrace] = useState(false);
+  const [properties, setProperties] = useState<string[]>([]);
+  const [savedTraces, setSavedTraces] = useState<[string, BigStepCause[]][]>([]);
+  const [activeProperty, setActiveProperty] = useState<number>(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,
+  }
+}