Compare commits

..

2 commits

7 changed files with 344 additions and 127 deletions

View file

@ -129,6 +129,8 @@ div.status {
border-radius: 50%; border-radius: 50%;
height: 12px; height: 12px;
width: 12px; width: 12px;
margin-left: 4px;
margin-right: 4px;
} }
div.status.violated { div.status.violated {

View file

@ -7,6 +7,8 @@ import AddIcon from '@mui/icons-material/Add';
import AutoAwesomeIcon from '@mui/icons-material/AutoAwesome'; import AutoAwesomeIcon from '@mui/icons-material/AutoAwesome';
import DeleteOutlineIcon from '@mui/icons-material/DeleteOutline'; import DeleteOutlineIcon from '@mui/icons-material/DeleteOutline';
import VisibilityIcon from '@mui/icons-material/Visibility'; 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 { Statechart } from "@/statecharts/abstract_syntax";
import { detectConnections } from "@/statecharts/detect_connections"; import { detectConnections } from "@/statecharts/detect_connections";
@ -30,6 +32,8 @@ import { VisualEditor, VisualEditorState } from "./VisualEditor/VisualEditor";
import { checkProperty, PropertyCheckResult } from "./check_property"; import { checkProperty, PropertyCheckResult } from "./check_property";
import { usePersistentState } from "./persistent_state"; import { usePersistentState } from "./persistent_state";
import { useEditor } from "./useEditor"; import { useEditor } from "./useEditor";
import { useUrlHashState } from "./useUrlHashState";
import { formatTime } from "@/util/util";
export type EditHistory = { export type EditHistory = {
current: VisualEditorState, current: VisualEditorState,
@ -47,7 +51,7 @@ const plants: [string, Plant<any, UniversalPlantState>][] = [
] ]
export type TraceItemError = { export type TraceItemError = {
cause: string, // event name, <init> or <timer> cause: BigStepCause, // event name, <init> or <timer>
simtime: number, simtime: number,
error: RuntimeError, error: RuntimeError,
} }
@ -58,9 +62,21 @@ type CoupledState = {
// plantCleanState: {[prop: string]: boolean|number}, // 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 = export type TraceItem =
{ kind: "error" } & TraceItemError { 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 = { export type TraceState = {
trace: [TraceItem, ...TraceItem[]], // non-empty trace: [TraceItem, ...TraceItem[]], // non-empty
@ -68,27 +84,46 @@ export type TraceState = {
}; };
export function App() { export function App() {
const [insertMode, setInsertMode] = usePersistentState<InsertMode>("insertMode", "and");
const [editHistory, setEditHistory] = useState<EditHistory|null>(null); const [editHistory, setEditHistory] = useState<EditHistory|null>(null);
const [trace, setTrace] = useState<TraceState|null>(null); const [trace, setTrace] = useState<TraceState|null>(null);
const [time, setTime] = useState<TimeMode>({kind: "paused", simtime: 0}); const [time, setTime] = useState<TimeMode>({kind: "paused", simtime: 0});
const [modal, setModal] = useState<ReactElement|null>(null); const [modal, setModal] = useState<ReactElement|null>(null);
const [plantName, setPlantName] = usePersistentState("plant", "dummy"); const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(setEditHistory);
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 editorState = editHistory && editHistory.current; const editorState = editHistory && editHistory.current;
const setEditorState = useCallback((cb: (value: VisualEditorState) => VisualEditorState) => { const setEditorState = useCallback((cb: (value: VisualEditorState) => VisualEditorState) => {
setEditHistory(historyState => historyState && ({...historyState, current: cb(historyState.current)})); setEditHistory(historyState => historyState && ({...historyState, current: cb(historyState.current)}));
}, [setEditHistory]); }, [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); const refRightSideBar = useRef<HTMLDivElement>(null);
// parse concrete syntax always: // parse concrete syntax always:
@ -105,8 +140,6 @@ export function App() {
}] : [], }] : [],
]; ];
const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(editorState, setEditHistory);
const scrollDownSidebar = useCallback(() => { const scrollDownSidebar = useCallback(() => {
if (autoScroll && refRightSideBar.current) { if (autoScroll && refRightSideBar.current) {
const el = refRightSideBar.current; const el = refRightSideBar.current;
@ -128,7 +161,7 @@ export function App() {
const onInit = useCallback(() => { const onInit = useCallback(() => {
if (cE === null) return; if (cE === null) return;
const metadata = {simtime: 0, cause: "<init>"}; const metadata = {simtime: 0, cause: {kind: "init" as const}};
try { try {
const [outputEvents, state] = cE.initial(); // may throw if initialing the statechart results in a RuntimeError const [outputEvents, state] = cE.initial(); // may throw if initialing the statechart results in a RuntimeError
setTrace({ setTrace({
@ -169,7 +202,7 @@ export function App() {
if (currentTraceItem !== null /*&& ast.inputEvents.some(e => e.event === inputEvent)*/) { if (currentTraceItem !== null /*&& ast.inputEvents.some(e => e.event === inputEvent)*/) {
if (currentTraceItem.kind === "bigstep") { if (currentTraceItem.kind === "bigstep") {
const simtime = getSimTime(time, Math.round(performance.now())); 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}); 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 nextTimeout = cE?.timeAdvance(currentTraceItem.state);
const raiseTimeEvent = () => { const raiseTimeEvent = () => {
appendNewConfig(nextTimeout, "<timer>", () => { appendNewConfig(nextTimeout, {kind: "timer", simtime: nextTimeout}, () => {
return cE.intTransition(currentTraceItem.state); return cE.intTransition(currentTraceItem.state);
}); });
} }
@ -207,7 +240,7 @@ export function App() {
} }
}, [time, currentTraceItem]); // <-- todo: is this really efficient? }, [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; let newItem: TraceItem;
const metadata = {simtime, cause} const metadata = {simtime, cause}
try { try {
@ -258,8 +291,6 @@ export function App() {
const highlightActive = (currentBigStep && currentBigStep.state.sc.mode) || new Set(); const highlightActive = (currentBigStep && currentBigStep.state.sc.mode) || new Set();
const highlightTransitions = currentBigStep && currentBigStep.state.sc.firedTransitions || []; 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; const speed = time.kind === "paused" ? 0 : time.scale;
@ -269,9 +300,53 @@ export function App() {
ast && autoConnect && autoDetectConns(ast, plant, setPlantConns); ast && autoConnect && autoDetectConns(ast, plant, setPlantConns);
}, [ast, plant, autoConnect]); }, [ast, plant, autoConnect]);
const [properties, setProperties] = usePersistentState<string[]>("properties", []);
const [propertyResults, setPropertyResults] = useState<PropertyCheckResult[] | null>(null); 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: // if some properties change, re-evaluate them:
useEffect(() => { useEffect(() => {
@ -395,39 +470,60 @@ export function App() {
{/* Properties */} {/* Properties */}
<PersistentDetails localStorageKey="showProperty" initiallyOpen={false}> <PersistentDetails localStorageKey="showProperty" initiallyOpen={false}>
<summary>properties</summary> <summary>properties</summary>
<div className="toolbar">
<button title="add property" onClick={() => setProperties(properties => [...properties, ""])}>
<AddIcon fontSize="small"/>
</button>
</div>
{properties.map((property, i) => { {properties.map((property, i) => {
const result = propertyResults && propertyResults[i]; const result = propertyResults && propertyResults[i];
let violated = null, propertyError = null; let violated = null, propertyError = null;
if (result) { if (result) {
violated = result[0] && !result[0][0].satisfied; violated = result[0] && result[0].length > 0 && !result[0][0].satisfied;
propertyError = result[1]; propertyError = result[1];
} }
return <div style={{width:'100%'}} key={i} className="toolbar"> return <div style={{width:'100%'}} key={i} className="toolbar">
<div className={"status" + (violated === null ? "" : (violated ? " violated" : " satisfied"))}></div> <div className={"status" + (violated === null ? "" : (violated ? " violated" : " satisfied"))}></div>
&nbsp;
<button title="see in trace (below)" className={activeProperty === i ? "active" : ""} onClick={() => setActiveProperty(i)}> <button title="see in trace (below)" className={activeProperty === i ? "active" : ""} onClick={() => setActiveProperty(i)}>
<VisibilityIcon fontSize="small"/> <VisibilityIcon fontSize="small"/>
</button> </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))}> <button title="delete this property" onClick={() => setProperties(properties => properties.toSpliced(i, 1))}>
<DeleteOutlineIcon fontSize="small"/> <DeleteOutlineIcon fontSize="small"/>
</button> </button>
{propertyError && <div style={{color: 'var(--error-color)'}}>{propertyError}</div>} {propertyError && <div style={{color: 'var(--error-color)'}}>{propertyError}</div>}
</div>; </div>;
})} })}
<div className="toolbar">
<button title="add property" onClick={() => setProperties(properties => [...properties, ""])}>
<AddIcon fontSize="small"/> add property
</button>
</div>
</PersistentDetails> </PersistentDetails>
{/* Traces */} {/* Traces */}
<details open={showExecutionTrace} onToggle={e => setShowExecutionTrace(e.newState === "open")}><summary>execution trace</summary> <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)}/> <div>
<label htmlFor="checkbox-show-plant-items">show plant steps</label> {savedTraces.map((savedTrace, i) =>
<input id="checkbox-autoscroll" type="checkbox" checked={autoScroll} onChange={e => setAutoScroll(e.target.checked)}/> <div key={i} className="toolbar">
<label htmlFor="checkbox-autoscroll">auto-scroll</label> <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> </details>
</div> </div>

View file

@ -3,7 +3,7 @@ import { Statechart, stateDescription } from "../statecharts/abstract_syntax";
import { Mode, RaisedEvent, RT_Event } from "../statecharts/runtime_types"; import { Mode, RaisedEvent, RT_Event } from "../statecharts/runtime_types";
import { formatTime } from "../util/util"; import { formatTime } from "../util/util";
import { TimeMode, timeTravel } from "../statecharts/time"; import { TimeMode, timeTravel } from "../statecharts/time";
import { TraceItem, TraceState } from "./App"; import { BigStepCause, TraceItem, TraceState } from "./App";
import { Environment } from "@/statecharts/environment"; import { Environment } from "@/statecharts/environment";
type RTHistoryProps = { type RTHistoryProps = {
@ -15,6 +15,8 @@ type RTHistoryProps = {
propertyTrace: {timestamp: number, satisfied: boolean}[] | null, 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] { function lookupPropertyStatus(simtime: number, propertyTrace: {timestamp: number, satisfied: boolean}[], startAt=0): [number, boolean | undefined] {
let i = startAt; let i = startAt;
while (i >= 0 && i < propertyTrace.length) { while (i >= 0 && i < propertyTrace.length) {
@ -55,16 +57,16 @@ export function RTHistory({trace, setTrace, ast, setTime, showPlantTrace, proper
if (!showPlantTrace && isPlantStep) { if (!showPlantTrace && isPlantStep) {
return <></> return <></>
} }
let propertyClasses = "status"; let propertyStatus: PropertyStatus = "unknown";
if (propertyTrace !== null) { if (propertyTrace !== null) {
let satisfied; let satisfied;
[j, satisfied] = lookupPropertyStatus(item.simtime, propertyTrace, j); [j, satisfied] = lookupPropertyStatus(item.simtime, propertyTrace, j);
// console.log(item.simtime, j, propertyTrace[j]); // console.log(item.simtime, j, propertyTrace[j]);
if (satisfied !== null && satisfied !== undefined) { 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") { else if (props.cause.kind === "input") {
return <>{props.cause.name}<RTEventParam param={props.cause.param}/></> return <>{props.cause.name}<RTEventParam param={props.cause.param}/></>
} }
console.log(props.cause); // console.log(props.cause);
throw new Error("unreachable"); throw new Error("unreachable");
} }
@ -86,7 +88,7 @@ function RTEventParam(props: {param?: any}) {
return <>{props.param !== undefined && <>({JSON.stringify(props.param)})</>}</>; 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") { if (item.kind === "bigstep") {
// @ts-ignore // @ts-ignore
const newStates = item.state.sc.mode.difference(prevItem?.state.sc.mode || new Set()); 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" : "")} className={"runtimeState" + (active ? " active" : "") + (isPlantStep ? " plantStep" : "")}
onMouseDown={useCallback(() => onMouseDown(idx, item.simtime), [idx, item.simtime])}> onMouseDown={useCallback(() => onMouseDown(idx, item.simtime), [idx, item.simtime])}>
<div> <div>
<div className={propertyClasses}/> <div className={"status " + propertyStatus}/>
&emsp; &emsp;
{formatTime(item.simtime)} {formatTime(item.simtime)}
&emsp; &emsp;
@ -115,7 +117,7 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
<div> <div>
{formatTime(item.simtime)} {formatTime(item.simtime)}
&emsp; &emsp;
<div className="inputEvent">{item.cause}</div> <div className="inputEvent"><ShowCause cause={item.cause}/></div>
</div> </div>
<div> <div>
{item.error.message} {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}) { function ShowEnvironment(props: {environment: Environment}) {
return <div>{ return <div>{

View file

@ -44,30 +44,6 @@ export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | Unst
</ul> </ul>
} }
</li>; </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'; import BoltIcon from '@mui/icons-material/Bolt';
@ -95,6 +71,7 @@ export function ShowInputEvents({inputEvents, onRaise, disabled, showKeys}: {inp
}); });
const onKeyDown = (e: KeyboardEvent) => { const onKeyDown = (e: KeyboardEvent) => {
// don't capture keyboard events when focused on an input element: // don't capture keyboard events when focused on an input element:
// @ts-ignore
if (["INPUT", "TEXTAREA", "SELECT"].includes(e.target?.tagName)) return; if (["INPUT", "TEXTAREA", "SELECT"].includes(e.target?.tagName)) return;
const n = (parseInt(e.key)+9) % 10; const n = (parseInt(e.key)+9) % 10;

View file

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

View file

@ -3,9 +3,8 @@ import { HISTORY_RADIUS } from "./parameters";
import { Dispatch, SetStateAction, useCallback, useEffect } from "react"; import { Dispatch, SetStateAction, useCallback, useEffect } from "react";
import { EditHistory } from "./App"; import { EditHistory } from "./App";
import { VisualEditorState } from "./VisualEditor/VisualEditor"; 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(() => { useEffect(() => {
console.info("Welcome to StateBuddy!"); 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 // append editor state to undo history
const makeCheckPoint = useCallback(() => { const makeCheckPoint = useCallback(() => {
setEditHistory(historyState => historyState && ({ setEditHistory(historyState => historyState && ({

185
src/App/useUrlHashState.ts Normal file
View file

@ -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,
}
}