Compare commits
2 commits
c7e661eb61
...
3c302a83c5
| Author | SHA1 | Date | |
|---|---|---|---|
| 3c302a83c5 | |||
| 49e701c7d7 |
7 changed files with 344 additions and 127 deletions
|
|
@ -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 {
|
||||||
|
|
|
||||||
166
src/App/App.tsx
166
src/App/App.tsx
|
|
@ -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>
|
||||||
|
|
||||||
<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>
|
||||||
|
|
||||||
|
<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>
|
||||||
|
|
||||||
|
<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>
|
||||||
|
 
|
||||||
|
<button title="save current trace" disabled={trace === null} onClick={() => onSaveTrace()}>
|
||||||
|
<SaveOutlinedIcon fontSize="small"/> save trace
|
||||||
|
</button>
|
||||||
|
</div>
|
||||||
</details>
|
</details>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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}/>
|
||||||
 
|
 
|
||||||
{formatTime(item.simtime)}
|
{formatTime(item.simtime)}
|
||||||
 
|
 
|
||||||
|
|
@ -115,7 +117,7 @@ export const RTHistoryItem = memo(function RTHistoryItem({ast, idx, item, prevIt
|
||||||
<div>
|
<div>
|
||||||
{formatTime(item.simtime)}
|
{formatTime(item.simtime)}
|
||||||
 
|
 
|
||||||
<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>{
|
||||||
|
|
|
||||||
|
|
@ -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> entry / <ShowAction action={action}/></div>
|
|
||||||
// )
|
|
||||||
// }
|
|
||||||
// {props.root.kind !== "pseudo" && props.root.exitActions.length>0 &&
|
|
||||||
// props.root.exitActions.map(action =>
|
|
||||||
// <div> 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 => <> <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;
|
||||||
|
|
|
||||||
|
|
@ -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];
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -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
185
src/App/useUrlHashState.ts
Normal 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,
|
||||||
|
}
|
||||||
|
}
|
||||||
Loading…
Add table
Add a link
Reference in a new issue