diff --git a/src/App/App.css b/src/App/App.css index 76f1272..d15f623 100644 --- a/src/App/App.css +++ b/src/App/App.css @@ -129,8 +129,6 @@ 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 e32ea12..e5a4a8c 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -7,8 +7,6 @@ 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"; @@ -32,8 +30,6 @@ 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, @@ -51,7 +47,7 @@ const plants: [string, Plant][] = [ ] export type TraceItemError = { - cause: BigStepCause, // event name, or + cause: string, // event name, or simtime: number, error: RuntimeError, } @@ -62,21 +58,9 @@ 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: BigStepCause, state: CoupledState, outputEvents: RaisedEvent[] }; +| { kind: "bigstep", simtime: number, cause: string, state: CoupledState, outputEvents: RaisedEvent[] }; export type TraceState = { trace: [TraceItem, ...TraceItem[]], // non-empty @@ -84,46 +68,27 @@ 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 {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(setEditHistory); + 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 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: @@ -140,6 +105,8 @@ export function App() { }] : [], ]; + const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(editorState, setEditHistory); + const scrollDownSidebar = useCallback(() => { if (autoScroll && refRightSideBar.current) { const el = refRightSideBar.current; @@ -161,7 +128,7 @@ export function App() { const onInit = useCallback(() => { if (cE === null) return; - const metadata = {simtime: 0, cause: {kind: "init" as const}}; + const metadata = {simtime: 0, cause: ""}; try { const [outputEvents, state] = cE.initial(); // may throw if initialing the statechart results in a RuntimeError setTrace({ @@ -202,7 +169,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, {kind: "input", simtime, eventName: inputEvent, param}, () => { + appendNewConfig(simtime, inputEvent, () => { return cE.extTransition(simtime, currentTraceItem.state, {kind: "input", name: inputEvent, param}); }); } @@ -217,7 +184,7 @@ export function App() { const nextTimeout = cE?.timeAdvance(currentTraceItem.state); const raiseTimeEvent = () => { - appendNewConfig(nextTimeout, {kind: "timer", simtime: nextTimeout}, () => { + appendNewConfig(nextTimeout, "", () => { return cE.intTransition(currentTraceItem.state); }); } @@ -240,7 +207,7 @@ export function App() { } }, [time, currentTraceItem]); // <-- todo: is this really efficient? - function appendNewConfig(simtime: number, cause: BigStepCause, computeNewState: () => [RaisedEvent[], CoupledState]) { + function appendNewConfig(simtime: number, cause: string, computeNewState: () => [RaisedEvent[], CoupledState]) { let newItem: TraceItem; const metadata = {simtime, cause} try { @@ -291,6 +258,8 @@ 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; @@ -300,53 +269,9 @@ export function App() { ast && autoConnect && autoDetectConns(ast, plant, setPlantConns); }, [ast, plant, autoConnect]); + const [properties, setProperties] = usePersistentState("properties", []); const [propertyResults, setPropertyResults] = useState(null); - - - 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}); - } - } + const [activeProperty, setActiveProperty] = usePersistentState("activeProperty", 0); // if some properties change, re-evaluate them: useEffect(() => { @@ -470,60 +395,39 @@ export function App() { {/* Properties */} properties +
+ +
{properties.map((property, i) => { const result = propertyResults && propertyResults[i]; let violated = null, propertyError = null; if (result) { - violated = result[0] && result[0].length > 0 && !result[0][0].satisfied; + violated = result[0] && !result[0][0].satisfied; propertyError = result[1]; } 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 -
- {savedTraces.map((savedTrace, i) => -
- -   - {(Math.floor(savedTrace[1].at(-1).simtime/1000))}s - ({savedTrace[1].length}) -   - setSavedTraces(savedTraces => savedTraces.toSpliced(i, 1, [e.target.value, savedTraces[i][1]]))}/> - -
- )} -
-
- setShowPlantTrace(e.target.checked)}/> - - setAutoScroll(e.target.checked)}/> - -   - -
+ setShowPlantTrace(e.target.checked)}/> + + setAutoScroll(e.target.checked)}/> +
diff --git a/src/App/RTHistory.tsx b/src/App/RTHistory.tsx index d834399..acce59c 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 { BigStepCause, TraceItem, TraceState } from "./App"; +import { TraceItem, TraceState } from "./App"; import { Environment } from "@/statecharts/environment"; type RTHistoryProps = { @@ -15,8 +15,6 @@ 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) { @@ -57,16 +55,16 @@ export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace, proper if (!showPlantTrace && isPlantStep) { return <> } - let propertyStatus: PropertyStatus = "unknown"; + 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) { - propertyStatus = (satisfied ? "satisfied" : "violated"); + propertyClasses += (satisfied ? " satisfied" : " violated"); } } - return ; + return ; }); } @@ -80,7 +78,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"); } @@ -88,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, propertyStatus}: {idx: number, ast: Statechart, item: TraceItem, prevItem?: TraceItem, isPlantStep: boolean, active: boolean, onMouseDown: (idx: number, timestamp: number) => void, propertyStatus: PropertyStatus}) { +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()); @@ -96,7 +94,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)}   @@ -117,7 +115,7 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
{formatTime(item.simtime)}   -
+
{item.cause}
{item.error.message} @@ -126,18 +124,6 @@ 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 8657331..3354c0f 100644 --- a/src/App/ShowAST.tsx +++ b/src/App/ShowAST.tsx @@ -44,6 +44,30 @@ 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'; @@ -71,7 +95,6 @@ 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 ff6e25a..9b571d2 100644 --- a/src/App/check_property.ts +++ b/src/App/check_property.ts @@ -70,12 +70,10 @@ 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 e1ca293..8ca0f52 100644 --- a/src/App/useEditor.ts +++ b/src/App/useEditor.ts @@ -3,8 +3,9 @@ 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(setEditHistory: Dispatch>) { +export function useEditor(editorState: VisualEditorState | null, setEditHistory: Dispatch>) { useEffect(() => { console.info("Welcome to StateBuddy!"); () => { @@ -12,6 +13,64 @@ export function useEditor(setEditHistory: Dispatch { + 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 deleted file mode 100644 index d00a629..0000000 --- a/src/App/useUrlHashState.ts +++ /dev/null @@ -1,185 +0,0 @@ -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