diff --git a/.gitignore b/.gitignore index d281236..a14702c 100644 --- a/.gitignore +++ b/.gitignore @@ -32,6 +32,3 @@ report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json # Finder (MacOS) folder config .DS_Store - -# When building the app, we include the git rev in the status bar. We do this by calling git and writing the rev to a file, which is then included by the app. -src/git-rev.txt diff --git a/assignment.html b/assignment.html new file mode 100644 index 0000000..b8252bb --- /dev/null +++ b/assignment.html @@ -0,0 +1,366 @@ + + + +

Practical stuff

+ + +

Goals

+

The goal of this assignment is to familiarize yourself with Statechart modeling, simulation, debugging and, + to a lesser extent, automatically checking requirements -specified as temporal logic formulas over behaviour traces- on your solution.

+ + + +

Getting Started

+

We will use the brand-new Statechart editor, simulation and testing environment StateBuddy, created by yours truly.

+ +

No need to install anything. StateBuddy runs in the browser.

+
+Note: StateBuddy will be updated from time to time, to fix bugs or add new features. +To make sure you have the latest version, in StateBuddy, use the shortcut Ctrl+Shift+R to refresh the page while clearing your browser cache. +StateBuddy was tested in Firefox 144.0 and Chromium 141.0.7390.107. +
+ +

Exercises

+

Before we start working on this assignment, we will solve 5 small exercises. +Each exercise shows you a small Statechart model, and asks a question about its behavior. +If you can solve the exercises, you will have a good (enough) understanding of the precise semantics of StateBuddy.

+ +

The exercises can be opened by clicking on their respective links:

+
    +
  1. + nested timed transitions
    2. +
  2. + parent-first
    3. +
  3. + order of orthogonal regions
    4. +
  4. + crossing orthogonal regions
    5. +
  5. + internal events (yes, there's a bug here that i should fix)
    6. +
+ + +
+ To solve the exercises, you must have a good understanding of the precise semantics of StateBuddy. + The semantics are as follows: + +

Example: + Consider the linked Statechart. + After initialization, the current states are: OrthogonalState, A, C, E. + Then, the Statechart remains idle until it receives an input event. Suppose at time T=5s, the input event e is received. This triggers the execution of an RTC step. + The RTC step starts with a fair-step, where regions r1, r2 and r3 (in that order) are allowed to fire at most one transition each. + Only r1 has an enabled transition (because event e is active), so only r1 fires. + During the firing of that transition, the internal event f is raised, an appended to the internal event queue. + The fair-step ends, and one more fair-step is executed, because the internal event queue is not empty. + So again, r1, r2 and r3 are allowed to fire at most one transition. + This time, the regions r2 and r3 will fire, because event f is active. + The second fair-step ends, and since the internal event queue is empty, the RTC step also ends. + Even though all transitions fired in a certain order, all of it happened at the same point in (simulated) time. + Now, the Statechart will again remain idle until another input event occurs. +

+ + + + + + + +
Time r1 r2 r3
=0Initialization enter A enter C enter E
>0 && <5sIdle
=5sRTC step (input=e) Fair-step (event=e) fire (exit A, raise f, enter B)
Fair-step (event=f) fire (exit C, enter D) fire (exit E, enter F)
=5sEnd of RTC step
+
+

+ Please remember that these precise semantics are specific to StateBuddy, although they are very similar to YAKINDU / Itemis Create. Other Statechart tools (e.g., STATEMATE, Rhapsody, StateFlow) have different semantics. +
+ +

Introduction to Assignment

+ +

You will use the Statecharts formalism to model the controller of a classic digital watch (before smart watches existed).

+ +
+ +
+
+ +

All user input happens through 4 buttons (one in each corner).

+

The watch can display 6 numbers, in the form HH:MM:SS when displaying the current time, or the time of the alarm, or in the form MM:SS:HS (HS means hectoseconds) when displaying the chronometer.

+

The watch has a background light that can be on or off.

+

The watch can make a beep-sound.

+

The time can be edited.

+

An alarm can be turned on or off. The alarm time can also be edited.

+

The chronometer can be started, paused, and reset.

+ + +

Interfaces

+

You will implement the plant (= digital watch) controller as a Statechart. The controller only talks to the plant via input-events and output-events. In StateBuddy, you can also interactively raise input events directly into the controller statechart (Debugger UI). Finally, the plant also has its own UI, which sends input events to the plant.

+

For the curious student: Yes, the (simulated) plant is also implemented as a (rather big) Statechart.

+
+ +
Overview of our simulated system-under-study.
+
+ +The plant can send the following events to the controller: + + + + + + + + + + + + + + + + +
Controller input event(s)Received when...
topLeftPressed, topRightPressed, bottomLeftPressed, bottomRightPressedone of the 4 buttons is pressed
topLeftReleased, topRightReleased, bottomLeftReleased, bottomRightReleasedone of the 4 buttons is released
alarmthe alarm should go off
+
+ +The controller can send the following events to the plant: + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Controller output event(s)Effect
lightOn, lightOffturns on / off the background light
beepmake a beep sound for 10ms
incTimeincrement the watch's time by one second
incChronoincrement the watch's chrono by 1/100 second
resetChronosets the chronometer back to 00:00:00
displayTimeputs the watch into a mode where it displays the current time
displayChronoputs the watch into a mode where it displays the chronometer
displayAlarmputs the watch into a mode where it displays the time of the alarm
setAlarm(boolean)turns the alarm on (true) or off (false). if the alarm is on, and the plant detects that the current time is equal to the alarm time, then the plant will immediately send the 'alarm' event (explained above) to the controller.
beginEditputs the plant into 'edit mode'. if the plant was displaying the current time, you can now edit the current time. if the plant was dispalying the alarm time, then you can now edit the alarm time. After entering edit mode, the 'hours' part of the display will start blinking, indicating that the 'hours' can be edited. +
endEditends the 'edit mode'. +
incSelectionwhen in 'edit mode', will increase the currently blinking part (i.e, hours, minutes or seconds) of the display by one
selectNextwhen in 'edit mode', will select the next item (hours -> minutes -> seconds -> hours) to edit
+ +

Behavioral Requirements

+
    +
  1. You may assume that initially, the plant is displaying the current time, the light is off, the alarm is off, the speaker is not beeping, and we are not in 'edit mode'. The chrono is zero and not running.
    2. + +
  2. For as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds.
    3. + +
  3. When displaying the time, or displaying the chrono, pressing the top-left button toggles between time and chrono mode.
    4. + +
  4. When in chrono mode, pressing the bottom-right button toggles the chrono between 'paused' and 'running'.
    5. +
  5. When in chrono mode, pressing the bottom-left button resets the chronometer to zero.
    6. + +
  6. When the chrono is running, the chronometer value is incremented by 1/100 second 100 times per second. The chronometer remains running until it is paused, even if we leave the chrono mode.
    7. + +
  7. The current time is incremented (ticks) by 1 second every second, even when we are not displaying the current time, except when we are editing the current time: then the time should not tick.
    8. + +
  8. Pressing the bottom-left button when the time is being displayed will show the alarm time and toggle the alarm (on/off).
    9. +
  9. If then, the bottom-left button is held pressed for 2 seconds, we go into alarm edit mode.
    10. + +
  10. Likewise, when displaying the current time, and pressing and holding the bottom-right button for 2 seconds, we go into time edit mode.
    11. + +
  11. In edit mode, pressing the bottom-left button will immediately increment the current selected (blinking) numbers.
    12. +
  12. In edit mode, holding the bottom-left button has the additional effect incrementing the current selected numbers every 100ms.
    13. + +
  13. In edit mode, pressing the bottom-right button will select the next numbers (hours -> minutes -> seconds -> hours).
    14. +
+ +

Starting point

+ +

Use this link to the starting point for this assignment.

+ +

Testing your solution

+

To test your solution, initialize the execution, and interact with the plant UI. The execution can run in (scaled) real-time, with the ability to pause/resume.

+

To gain more confidence that you correctly implemented the requirements, you can write Metric Temporal Logic (MTL) properties. An example of such a property is: + 

G (topRightPressed -> (lightOn U (~topRightPressed & F[0,2] lightOn)))
+meaning: "as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds" AKA Requirement 1. +

+ +
Tip: ChatGPT is quite good at translating natural language to MTL properties!
+ +

Note that none of these testing approaches are exhaustive (unlike model checking, which is exhaustive). Any property you write will only be checked on the current simulation trace.

+ +

Report

+

You are also required to write a small(*) (HTML or PDF) report.

+

(*) I don't have time to read 100 pages!

+

It must include the following:

+ + + +

What is expected

+

Your solution needs to be precisely correct: superficially correct behavior when running the generated code with the GUI (e.g., seeing the water levels change) is not enough: the timing-related requirements are exact.

+

The assignment has been designed specifically to encourage use of as many Statechart features as possible:

+ +

Make sure you understand these features, and use them, where you think they are appropriate.

+

To give you an indication of the complexity, my own solution consists of 19 AND-states, 10 OR-states, and 36 transitions.

+ + +

Additional resources

+ + + diff --git a/package.json b/package.json index 188c9c2..73cf039 100644 --- a/package.json +++ b/package.json @@ -7,12 +7,13 @@ "module": "src/index.tsx", "scripts": { "dev": "bun --hot src/index.tsx", - "build": "git rev-parse HEAD > src/git-rev.txt && NODE_ENV=production bun build ./src/index.html --outdir=dist --sourcemap --target=browser --minify --define:process.env.NODE_ENV='\"production\"' --env='BUN_PUBLIC_*'", + "build": "NODE_ENV=production bun build ./src/index.html --outdir=dist --sourcemap --target=browser --minify --define:process.env.NODE_ENV='\"production\"' --env='BUN_PUBLIC_*'", "start": "NODE_ENV=production bun src/index.tsx" }, "dependencies": { "@fontsource/roboto": "^5.2.8", "@mui/icons-material": "^7.3.4", + // "argus-wasm": "git+https://deemz.org/git/joeri/argus-wasm.git#a4491b3433d48aa1f941bd5ad37b36f819d3b2ac", "react": "^19.2.0", "react-dom": "^19.2.0" }, diff --git a/src/App/AST.css b/src/App/AST.css new file mode 100644 index 0000000..f2081f6 --- /dev/null +++ b/src/App/AST.css @@ -0,0 +1,125 @@ +details.active { + border: rgb(192, 125, 0); + background-color:rgb(255, 251, 244); + filter: drop-shadow( 0px 0px 3px rgba(192, 125, 0, 0.856)); +} + +details > summary { + padding: 2px; +} + +/* these two rules add a bit of padding to an opened
node */ +/* details:open > summary:has(+ *) { + margin-bottom: 4px; +} +details:open:has(>summary:has(+ *)) { + padding-bottom: 8px; +} */ + +details > summary:hover { + background-color: #eee; + cursor: default; +} + +.errorStatus details > summary:hover { + background-color: rgb(102, 0, 0); +} + +.stateTree > * { + padding-left: 10px; + /* border: 1px black solid; */ + background-color: white; + /* margin-bottom: 4px; */ + /* padding-right: 2px; */ + /* padding-top: 2px; */ + /* padding-bottom: 2px; */ + /* color: black; */ + /* width: fit-content; */ + /* border-radius: 10px; */ +} + +/* if
has no children (besides the obvious child), then hide the marker */ +/* details:not(:has(:not(summary))) > summary::marker { + content: " "; +} */ + +.outputEvent { + border: 1px black solid; + border-radius: 6px; + /* margin-left: 4px; */ + padding-left: 2px; + padding-right: 2px; + background-color: rgb(230, 249, 255); + color: black; + display: inline-block; +} + +.internalEvent { + border: 1px black solid; + border-radius: 6px; + /* margin-left: 4px; */ + padding-left: 2px; + padding-right: 2px; + background-color: rgb(255, 218, 252); + color: black; + display: inline-block; +} + +.inputEvent { + border: 1px black solid; + border-radius: 6px; + /* margin-left: 4px; */ + padding-left: 2px; + padding-right: 2px; + background-color: rgb(224, 247, 209); + color: black; + display: inline-block; +} +.inputEvent:disabled { + color: darkgrey; +} +.inputEvent * { + vertical-align: middle; +} +button.inputEvent:hover:not(:disabled) { + background-color: rgb(195, 224, 176); +} +button.inputEvent:active:not(:disabled) { + background-color: rgb(176, 204, 158); +} + +.activeState { + border: rgb(192, 125, 0); + background-color:rgb(255, 251, 244); + filter: drop-shadow( 0px 0px 3px rgba(192, 125, 0, 0.856)); + border-radius: 6px; + margin-left: 4px; + padding-left: 2px; + padding-right: 2px; + display: inline-block; +} + +/* hr { + display: block; + height: 1px; + border: 0; + border-top: 1px solid #ccc; + margin: 0; + margin-top: -1px; + margin-bottom: -5px; + padding: 0; + z-index: -1; +} */ + +ul { + list-style-type: circle; + margin-block-start: 0; + margin-block-end: 0; + padding-inline-start: 24px; + /* list-style-position: ; */ +} + +.shadowBelow { + box-shadow: 0 -5px 5px 5px rgba(0, 0, 0, 0.4); + z-index: 1; +} diff --git a/src/App/App.css b/src/App/App.css index 2929afe..51defe8 100644 --- a/src/App/App.css +++ b/src/App/App.css @@ -1,44 +1,61 @@ +/* details { + padding-left: 20; +} +summary { + margin-left: -20; +} */ + details:has(+ details) { - border-bottom: 1px var(--separator-color) solid; + border-bottom: 1px lightgrey solid; } .runtimeState { padding: 4px; + /* padding-left: 4px; + padding-right: 4px; + padding-top: 2px; + padding-bottom: 2px; */ } .runtimeState:has(+.runtimeState) { - border-bottom: 1px var(--separator-color) solid; + border-bottom: 1px lightgrey solid; } .runtimeState:has(+.runtimeState.active) { border-bottom: 0; } .runtimeState:hover { - background-color: var(--light-accent-color); + /* background-color: rgba(255, 140, 0, 0.2); */ + background-color: rgba(0,0,255,0.2); cursor: pointer; } .runtimeState.active { - background-color: var(--light-accent-color); - border: solid var(--accent-border-color) 1px; + background-color: rgba(0,0,255,0.2); + border: solid blue 1px; } .runtimeState.plantStep:not(.active) { - background-color: var(--inactive-bg-color); + background-color: #f7f7f7; } .runtimeState.plantStep * { - color: var(--inactive-fg-color); + color: grey; } .runtimeState.runtimeError { - background-color: var(--error-bg-color); - color: var(--error-color); /* used to be darkred, but this one's a bit lighter */ + background-color: lightpink; + color: darkred; } .runtimeState.runtimeError.active { - border-color: var(--error-color);/* used to be darkred, but this one's a bit lighter */ + border-color: darkred; } +/* details:not(:has(details)) > summary::marker { + color: white; +} */ + .readonlyTextBox { width: 56; + background-color:"#eee"; text-align: "right"; } @@ -47,7 +64,7 @@ details:has(+ details) { } .toolbar input { - height: 22px; + height: 20px; } .toolbar div { vertical-align: bottom; @@ -60,6 +77,23 @@ details:has(+ details) { display: inline-block; } +button { + background-color: #fcfcfc; + border: 1px lightgrey solid; +} + +button:not(:disabled):hover { + background-color: rgba(0, 0, 255, 0.2); +} + +button.active { + border: solid blue 1px; + background-color: rgba(0,0,255,0.2); + /* margin-right: 1px; */ + /* margin-left: 0; */ + color: black; +} + .modalOuter { position: absolute; width: 100%; @@ -68,7 +102,7 @@ details:has(+ details) { justify-content: center; align-items: center; text-align: center; - background-color: var(--modal-backdrop-color); + background-color: rgba(200,200,200,0.7); z-index: 1000; } @@ -76,7 +110,7 @@ details:has(+ details) { position: relative; text-align: center; display: inline-block; - background-color: var(--background-color); + background-color: white; max-height: 100vh; overflow: auto; } @@ -94,7 +128,7 @@ div.stackHorizontal { div.status { display: inline-block; vertical-align: middle; - background-color: var(--status-inactive-color); + background-color: grey; border-radius: 50%; height: 12px; width: 12px; @@ -107,6 +141,6 @@ div.status.violated { } div.status.satisfied { - background-color: var(--status-ok-color); + background-color: forestgreen; } diff --git a/src/App/App.tsx b/src/App/App.tsx index 9855a60..b18d96a 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -1,23 +1,36 @@ import "../index.css"; import "./App.css"; -import { ReactElement, useCallback, useEffect, useMemo, useRef, useState } from "react"; +import { Dispatch, ReactElement, SetStateAction, useCallback, useEffect, useMemo, useRef, useState } from "react"; +import AddIcon from '@mui/icons-material/Add'; +import AutoAwesomeIcon from '@mui/icons-material/AutoAwesome'; +import CachedOutlinedIcon from '@mui/icons-material/CachedOutlined'; +import DeleteOutlineIcon from '@mui/icons-material/DeleteOutline'; +import SaveOutlinedIcon from '@mui/icons-material/SaveOutlined'; +import VisibilityIcon from '@mui/icons-material/Visibility'; + +import { Statechart } from "@/statecharts/abstract_syntax"; import { detectConnections } from "@/statecharts/detect_connections"; +import { Conns, coupledExecution, statechartExecution } from "@/statecharts/timed_reactive"; +import { RuntimeError } from "../statecharts/interpreter"; import { parseStatechart } from "../statecharts/parser"; -import { BottomPanel } from "./BottomPanel/BottomPanel"; -import { defaultSideBarState, SideBar, SideBarState } from "./SideBar/SideBar"; -import { InsertMode } from "./TopPanel/InsertModes"; +import { BigStep, RaisedEvent } from "../statecharts/runtime_types"; +import { getSimTime, getWallClkDelay, TimeMode } from "../statecharts/time"; +import { BottomPanel } from "./BottomPanel"; +import { PersistentDetails, PersistentDetailsLocalStorage } from "./PersistentDetails"; +import { digitalWatchPlant } from "./Plant/DigitalWatch/DigitalWatch"; +import { dummyPlant } from "./Plant/Dummy/Dummy"; +import { microwavePlant } from "./Plant/Microwave/Microwave"; +import { Plant } from "./Plant/Plant"; +import { trafficLightPlant } from "./Plant/TrafficLight/TrafficLight"; +import { RTHistory } from "./RTHistory"; +import { ShowAST, ShowInputEvents, ShowInternalEvents, ShowOutputEvents } from "./ShowAST"; import { TopPanel } from "./TopPanel/TopPanel"; import { VisualEditor, VisualEditorState } from "./VisualEditor/VisualEditor"; -import { makeAllSetters } from "./makePartialSetter"; -import { useEditor } from "./hooks/useEditor"; -import { useSimulator } from "./hooks/useSimulator"; -import { useUrlHashState } from "../hooks/useUrlHashState"; -import { plants } from "./plants"; -import { emptyState } from "@/statecharts/concrete_syntax"; -import { ModalOverlay } from "./Overlays/ModalOverlay"; -import { FindReplace } from "./BottomPanel/FindReplace"; +import { checkProperty, PropertyCheckResult } from "./check_property"; +import { useEditor } from "./useEditor"; +import { useUrlHashState } from "./useUrlHashState"; export type EditHistory = { current: VisualEditorState, @@ -25,87 +38,110 @@ export type EditHistory = { future: VisualEditorState[], } -export type AppState = { - showKeys: boolean, - zoom: number, - insertMode: InsertMode, - showFindReplace: boolean, - findText: string, - replaceText: string, -} & SideBarState; +type UniversalPlantState = {[property: string]: boolean|number}; -const defaultAppState: AppState = { - showKeys: true, - zoom: 1, - insertMode: 'and', - showFindReplace: false, - findText: "", - replaceText: "", - ...defaultSideBarState, +const plants: [string, Plant][] = [ + ["dummy", dummyPlant], + ["microwave", microwavePlant as unknown as Plant], + ["digital watch", digitalWatchPlant as unknown as Plant], + ["traffic light", trafficLightPlant as unknown as Plant], +] + +export type TraceItemError = { + cause: BigStepCause, // event name, or + simtime: number, + error: RuntimeError, } -export type LightMode = "light" | "auto" | "dark"; +type CoupledState = { + sc: BigStep, + plant: BigStep, + // plantCleanState: {[prop: string]: boolean|number}, +}; + +export type BigStepCause = { + kind: "init", + simtime: 0, +} | { + 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[] }; + +export type TraceState = { + trace: [TraceItem, ...TraceItem[]], // non-empty + idx: number, +}; export function App() { const [editHistory, setEditHistory] = useState(null); + const [trace, setTrace] = useState(null); + const [time, setTime] = useState({kind: "paused", simtime: 0}); const [modal, setModal] = useState(null); - const {commitState, replaceState, onRedo, onUndo, onRotate} = useEditor(setEditHistory); + const {makeCheckPoint, onRedo, onUndo, onRotate} = useEditor(setEditHistory); const editorState = editHistory && editHistory.current; const setEditorState = useCallback((cb: (value: VisualEditorState) => VisualEditorState) => { setEditHistory(historyState => historyState && ({...historyState, current: cb(historyState.current)})); }, [setEditHistory]); + const { + autoConnect, + setAutoConnect, + autoScroll, + setAutoScroll, + plantConns, + setPlantConns, + showKeys, + setShowKeys, + zoom, + setZoom, + insertMode, + setInsertMode, + plantName, + setPlantName, + showConnections, + setShowConnections, + showProperties, + setShowProperties, + 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: const conns = useMemo(() => editorState && detectConnections(editorState), [editorState]); const parsed = useMemo(() => editorState && conns && parseStatechart(editorState, conns), [editorState, conns]); const ast = parsed && parsed[0]; + const syntaxErrors = parsed && parsed[1] || []; + const currentTraceItem = trace && trace.trace[trace.idx]; + const allErrors = [ + ...syntaxErrors, + ...(currentTraceItem && currentTraceItem.kind === "error") ? [{ + message: currentTraceItem.error.message, + shapeUid: currentTraceItem.error.highlight[0], + }] : [], + ]; - const [appState, setAppState] = useState(defaultAppState); - - const persist = useUrlHashState( - recoveredState => { - if (recoveredState === null) { - setEditHistory(() => ({current: emptyState, history: [], future: []})); - } - // we support two formats - // @ts-ignore - else if (recoveredState.nextID) { - // old format - setEditHistory(() => ({current: recoveredState as VisualEditorState, history: [], future: []})); - } - else { - // new format - // @ts-ignore - if (recoveredState.editorState !== undefined) { - const {editorState, ...appState} = recoveredState as AppState & {editorState: VisualEditorState}; - setEditHistory(() => ({current: editorState, history: [], future: []})); - setAppState(defaultAppState => Object.assign({}, defaultAppState, appState)); - } - } - }, - ); - - useEffect(() => { - const timeout = setTimeout(() => { - if (editorState !== null) { - console.log('persisting state to url'); - persist({editorState, ...appState}); - } - }, 100); - return () => clearTimeout(timeout); - }, [editorState, appState]); - - const { - autoScroll, - plantConns, - plantName, - } = appState; - - const plant = plants.find(([pn, p]) => pn === plantName)![1]; - - const refRightSideBar = useRef(null); const scrollDownSidebar = useCallback(() => { if (autoScroll && refRightSideBar.current) { const el = refRightSideBar.current; @@ -116,91 +152,492 @@ export function App() { } }, [refRightSideBar.current, autoScroll]); - const simulator = useSimulator(ast, plant, plantConns, scrollDownSidebar); - - // console.log('render app', {ast, plant, appState}); - // useDetectChange(ast, 'ast'); - // useDetectChange(plant, 'plant'); - // useDetectChange(scrollDownSidebar, 'scrollDownSidebar'); - // useDetectChange(appState, 'appState'); - // useDetectChange(simulator.time, 'simulator.time'); - // useDetectChange(simulator.trace, 'simulator.trace'); + // coupled execution + const cE = useMemo(() => ast && coupledExecution({ + sc: statechartExecution(ast), + plant: plant.execution, + }, { + ...plantConns, + ...Object.fromEntries(ast.inputEvents.map(({event}) => ["debug."+event, ['sc',event] as [string,string]])), + }), [ast]); - const setters = makeAllSetters(setAppState, Object.keys(appState) as (keyof AppState)[]); + const onInit = useCallback(() => { + if (cE === null) return; + const metadata = {simtime: 0, cause: {kind: "init" as const, simtime: 0 as const}}; + try { + const [outputEvents, state] = cE.initial(); // may throw if initialing the statechart results in a RuntimeError + setTrace({ + trace: [{kind: "bigstep", ...metadata, state, outputEvents}], + idx: 0, + }); + } + catch (error) { + if (error instanceof RuntimeError) { + setTrace({ + trace: [{kind: "error", ...metadata, error}], + idx: 0, + }); + } + else { + throw error; // probably a bug in the interpreter + } + } + setTime(time => { + if (time.kind === "paused") { + return {...time, simtime: 0}; + } + else { + return {...time, since: {simtime: 0, wallclktime: performance.now()}}; + } + }); + scrollDownSidebar(); + }, [cE, scrollDownSidebar]); + + const onClear = useCallback(() => { + setTrace(null); + setTime({kind: "paused", simtime: 0}); + }, [setTrace, setTime]); + + // raise input event, producing a new runtime configuration (or a runtime error) + const onRaise = (inputEvent: string, param: any) => { + if (cE === null) return; + 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}, () => { + return cE.extTransition(simtime, currentTraceItem.state, {kind: "input", name: inputEvent, param}); + }); + } + } + }; + + // timer elapse events are triggered by a change of the simulated time (possibly as a scheduled JS event loop timeout) + useEffect(() => { + let timeout: NodeJS.Timeout | undefined; + if (currentTraceItem !== null && cE !== null) { + if (currentTraceItem.kind === "bigstep") { + const nextTimeout = cE?.timeAdvance(currentTraceItem.state); + + const raiseTimeEvent = () => { + appendNewConfig(nextTimeout, {kind: "timer", simtime: nextTimeout}, () => { + return cE.intTransition(currentTraceItem.state); + }); + } + + if (time.kind === "realtime") { + const wallclkDelay = getWallClkDelay(time, nextTimeout, Math.round(performance.now())); + if (wallclkDelay !== Infinity) { + timeout = setTimeout(raiseTimeEvent, wallclkDelay); + } + } + else if (time.kind === "paused") { + if (nextTimeout <= time.simtime) { + raiseTimeEvent(); + } + } + } + } + return () => { + if (timeout) clearTimeout(timeout); + } + }, [time, currentTraceItem]); // <-- todo: is this really efficient? + + function appendNewConfig(simtime: number, cause: BigStepCause, computeNewState: () => [RaisedEvent[], CoupledState]) { + let newItem: TraceItem; + const metadata = {simtime, cause} + try { + const [outputEvents, state] = computeNewState(); // may throw RuntimeError + newItem = {kind: "bigstep", ...metadata, state, outputEvents}; + } + catch (error) { + if (error instanceof RuntimeError) { + newItem = {kind: "error", ...metadata, error}; + // also pause the simulation, for dramatic effect: + setTime({kind: "paused", simtime}); + } + else { + throw error; + } + } + // @ts-ignore + setTrace(trace => ({ + trace: [ + ...trace!.trace.slice(0, trace!.idx+1), // remove everything after current item + newItem, + ], + // idx: 0, + idx: trace!.idx+1, + })); + scrollDownSidebar(); + } + + const onBack = useCallback(() => { + if (trace !== null) { + setTime(() => { + if (trace !== null) { + return { + kind: "paused", + simtime: trace.trace[trace.idx-1].simtime, + } + } + return { kind: "paused", simtime: 0 }; + }); + setTrace({ + ...trace, + idx: trace.idx-1, + }); + } + }, [trace]); - const syntaxErrors = parsed && parsed[1] || []; - const currentTraceItem = simulator.trace && simulator.trace.trace[simulator.trace.idx]; const currentBigStep = currentTraceItem && currentTraceItem.kind === "bigstep" && currentTraceItem; - const allErrors = [ - ...syntaxErrors, - ...(currentTraceItem && currentTraceItem.kind === "error") ? [{ - message: currentTraceItem.error.message, - shapeUid: currentTraceItem.error.highlight[0], - }] : [], - ]; const highlightActive = (currentBigStep && currentBigStep.state.sc.mode) || new Set(); const highlightTransitions = currentBigStep && currentBigStep.state.sc.firedTransitions || []; + + const speed = time.kind === "paused" ? 0 : time.scale; + const plantState = currentBigStep && currentBigStep.state.plant || plant.execution.initial()[1]; - return
- - {/* top-to-bottom: everything -> bottom panel */} -
+ useEffect(() => { + ast && autoConnect && autoDetectConns(ast, plant, setPlantConns); + }, [ast, plant, autoConnect]); - {/* left-to-right: main -> sidebar */} -
+ const [propertyResults, setPropertyResults] = useState(null); - {/* top-to-bottom: top bar, editor */} -
- {/* Top bar */} -
- {editHistory && } -
- {/* Editor */} -
- {editorState && conns && syntaxErrors && - } -
- - {appState.showFindReplace && -
- setters.setShowFindReplace(false)}/> -
- } -
+ const onSaveTrace = () => { + if (trace) { + setSavedTraces(savedTraces => [ + ...savedTraces, + ["untitled", trace.trace.map((item) => item.cause)] as [string, BigStepCause[]], + ]); + } + } - {/* Right: sidebar */} -
-
- -
-
+ const onReplayTrace = (causes: BigStepCause[]) => { + if (cE) { + function run_until(simtime: number) { + while (true) { + const nextTimeout = cE!.timeAdvance(lastState); + if (nextTimeout > simtime) { + break; + } + const [outputEvents, coupledState] = cE!.intTransition(lastState); + lastState = coupledState; + lastSimtime = nextTimeout; + newTrace.push({kind: "bigstep", simtime: nextTimeout, state: coupledState, outputEvents, cause: {kind: "timer", simtime: nextTimeout}}); + } + } + const [outputEvents, coupledState] = cE.initial(); + const newTrace = [{kind: "bigstep", simtime: 0, state: coupledState, outputEvents, cause: {kind: "init"} as BigStepCause} as TraceItem] as [TraceItem, ...TraceItem[]]; + let lastState = coupledState; + let lastSimtime = 0; + for (const cause of causes) { + if (cause.kind === "input") { + run_until(cause.simtime); // <-- just make sure we haven't missed any timers elapsing + // @ts-ignore + const [outputEvents, coupledState] = cE.extTransition(cause.simtime, newTrace.at(-1)!.state, {kind: "input", name: cause.eventName, param: cause.param}); + lastState = coupledState; + lastSimtime = cause.simtime; + newTrace.push({kind: "bigstep", simtime: cause.simtime, state: coupledState, outputEvents, cause}); + } + else if (cause.kind === "timer") { + run_until(cause.simtime); + } + } + setTrace({trace: newTrace, idx: newTrace.length-1}); + setTime({kind: "paused", simtime: lastSimtime}); + } + } + + // if some properties change, re-evaluate them: + useEffect(() => { + let timeout: NodeJS.Timeout; + if (trace) { + setPropertyResults(null); + timeout = setTimeout(() => { + Promise.all(properties.map((property, i) => { + return checkProperty(plant, property, trace.trace); + })) + .then(results => { + setPropertyResults(results); + }) + }) + } + return () => clearTimeout(timeout); + }, [properties, trace, plant]); + + return <> + + {/* Modal dialog */} + {modal &&
setModal(null)}> +
+ e.stopPropagation()}> + {modal} + +
+
} + + {/* top-to-bottom: everything -> bottom panel */} +
+ + {/* left-to-right: main -> sidebar */} +
+ + {/* top-to-bottom: top bar, editor */} +
+ {/* Top bar */} +
+ {editHistory && }
- - {/* Bottom panel */} -
- {syntaxErrors && } + {/* Editor */} +
+ {editorState && conns && syntaxErrors && + }
- -
; + + {/* Right: sidebar */} +
+
+
+ {/* State tree */} + + state tree +
    + {ast && } +
+ + {/* Input events */} + + input events + {ast && onRaise("debug."+e,p)} + disabled={trace===null || trace.trace[trace.idx].kind === "error"} + showKeys={showKeys}/>} + + {/* Internal events */} + + internal events + {ast && } + + {/* Output events */} + + output events + {ast && } + + {/* Plant */} + + plant + +
+ {/* Render plant */} + { onRaise("plant.ui."+e.name, e.param)} + />} + + {/* Connections */} + + connections + + {ast && ConnEditor(ast, plant, plantConns, setPlantConns)} + + {/* Properties */} +
setShowProperties(e.newState === "open")}> + properties + {plant &&
+ available signals: +   + {plant.signals.join(', ')} +
} + {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; + propertyError = result[1]; + } + return
+
+ + 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)}/> + +   + +
+
+
+ + {/* We cheat a bit, and render the execution trace depending on whether the
above is 'open' or not, rather than putting it as a child of the
. We do this because only then can we get the execution trace to scroll without the rest scrolling as well. */} + {showExecutionTrace && +
+
+ {ast && } +
+
} +
+
+
+
+
+ + {/* Bottom panel */} +
+ {syntaxErrors && } +
+
+ ; +} + +function autoDetectConns(ast: Statechart, plant: Plant, setPlantConns: Dispatch>) { + for (const {event: a} of plant.uiEvents) { + for (const {event: b} of plant.inputEvents) { + if (a === b) { + setPlantConns(conns => ({...conns, ['plant.ui.'+a]: ['plant', b]})); + break; + } + } + for (const {event: b} of ast.inputEvents) { + if (a === b) { + setPlantConns(conns => ({...conns, ['plant.ui.'+a]: ['sc', b]})); + } + } + } + for (const a of ast.outputEvents) { + for (const {event: b} of plant.inputEvents) { + if (a === b) { + setPlantConns(conns => ({...conns, ['sc.'+a]: ['plant', b]})); + } + } + } + for (const {event: a} of plant.outputEvents) { + for (const {event: b} of ast.inputEvents) { + if (a === b) { + setPlantConns(conns => ({...conns, ['plant.'+a]: ['sc', b]})); + } + } + } +} + + +function ConnEditor(ast: Statechart, plant: Plant, plantConns: Conns, setPlantConns: Dispatch>) { + const plantInputs = <>{plant.inputEvents.map(e => )} + const scInputs = <>{ast.inputEvents.map(e => )}; + return <> + + {/* SC output events can go to Plant */} + {[...ast.outputEvents].map(e =>
+ + +
)} + + {/* Plant output events can go to Statechart */} + {[...plant.outputEvents.map(e =>
+ + +
)]} + + {/* Plant UI events typically go to the Plant */} + {plant.uiEvents.map(e =>
+ + +
)} + ; } export default App; + diff --git a/src/App/BottomPanel.css b/src/App/BottomPanel.css new file mode 100644 index 0000000..92c1a48 --- /dev/null +++ b/src/App/BottomPanel.css @@ -0,0 +1,10 @@ +.errorStatus { + /* background-color: rgb(230,0,0); */ + background-color: var(--error-color); + color: white; +} + +.bottom { + border-top: 1px lightgrey solid; + background-color: rgb(255, 249, 235); +} \ No newline at end of file diff --git a/src/App/BottomPanel.tsx b/src/App/BottomPanel.tsx new file mode 100644 index 0000000..2f84992 --- /dev/null +++ b/src/App/BottomPanel.tsx @@ -0,0 +1,39 @@ +import { useEffect, useState } from "react"; +import { TraceableError } from "../statecharts/parser"; + +import "./BottomPanel.css"; + +import logo from "../../artwork/logo-playful.svg"; +import { PersistentDetailsLocalStorage } from "./PersistentDetails"; + +export function BottomPanel(props: {errors: TraceableError[]}) { + const [greeting, setGreeting] = useState( +
+ + Welcome to + +
); + + useEffect(() => { + setTimeout(() => { + setGreeting(<>); + }, 2000); + }, []); + + return
+ {greeting} + {props.errors.length > 0 && +
+ + {props.errors.length} errors +
+ {props.errors.map(({message, shapeUid})=> +
+ {shapeUid}: {message} +
)} +
+ +
+ } +
; +} \ No newline at end of file diff --git a/src/App/BottomPanel/BottomPanel.css b/src/App/BottomPanel/BottomPanel.css deleted file mode 100644 index 098ef48..0000000 --- a/src/App/BottomPanel/BottomPanel.css +++ /dev/null @@ -1,15 +0,0 @@ -.errorStatus { - /* background-color: rgb(230,0,0); */ - background-color: var(--error-color); - color: var(--background-color); -} - -.greeter { - /* border-top: 1px var(--separator-color) solid; */ - background-color: var(--greeter-bg-color); -} - -.bottom { - border-top: 1px var(--separator-color) solid; - background-color: var(--bottom-panel-bg-color); -} \ No newline at end of file diff --git a/src/App/BottomPanel/BottomPanel.tsx b/src/App/BottomPanel/BottomPanel.tsx deleted file mode 100644 index d1f5e3a..0000000 --- a/src/App/BottomPanel/BottomPanel.tsx +++ /dev/null @@ -1,48 +0,0 @@ -import { Dispatch, useEffect, useState } from "react"; -import { TraceableError } from "../../statecharts/parser"; - -import "./BottomPanel.css"; - -import { PersistentDetailsLocalStorage } from "../Components/PersistentDetails"; -import { Logo } from "@/App/Logo/Logo"; -import { AppState } from "../App"; -import { FindReplace } from "./FindReplace"; -import { VisualEditorState } from "../VisualEditor/VisualEditor"; -import { Setters } from "../makePartialSetter"; - -import gitRev from "@/git-rev.txt"; - -export function BottomPanel(props: {errors: TraceableError[], setEditorState: Dispatch<(state: VisualEditorState) => VisualEditorState>} & AppState & Setters) { - const [greeting, setGreeting] = useState( -
- - Welcome to - -
); - - useEffect(() => { - setTimeout(() => { - setGreeting(<>); - }, 2000); - }, []); - - return
- {/* {props.showFindReplace && -
- props.setShowFindReplace(false)}/> -
- } */} -
- - {props.errors.length} errors -
- {props.errors.map(({message, shapeUid})=> -
- {shapeUid}: {message} -
)} -
- -
- {greeting} -
; -} diff --git a/src/App/BottomPanel/FindReplace.tsx b/src/App/BottomPanel/FindReplace.tsx deleted file mode 100644 index 4ea9326..0000000 --- a/src/App/BottomPanel/FindReplace.tsx +++ /dev/null @@ -1,48 +0,0 @@ -import { Dispatch, useCallback, useEffect } from "react"; -import { VisualEditorState } from "../VisualEditor/VisualEditor"; -import { usePersistentState } from "@/hooks/usePersistentState"; - -import CloseIcon from '@mui/icons-material/Close'; -import SwapHorizIcon from '@mui/icons-material/SwapHoriz'; -import { useShortcuts } from "@/hooks/useShortcuts"; - -type FindReplaceProps = { - setCS: Dispatch<(oldState: VisualEditorState) => VisualEditorState>, - // setModal: (modal: null) => void; - hide: () => void, -}; - -export function FindReplace({setCS, hide}: FindReplaceProps) { - const [findTxt, setFindText] = usePersistentState("findTxt", ""); - const [replaceTxt, setReplaceTxt] = usePersistentState("replaceTxt", ""); - - const onReplace = useCallback(() => { - setCS(cs => { - return { - ...cs, - texts: cs.texts.map(txt => ({ - ...txt, - text: txt.text.replaceAll(findTxt, replaceTxt) - })), - }; - }); - }, [findTxt, replaceTxt]); - - useShortcuts([ - {keys: ["Enter"], action: onReplace}, - ]) - - const onSwap = useCallback(() => { - setReplaceTxt(findTxt); - setFindText(replaceTxt); - }, [findTxt, replaceTxt]); - - return
- setFindText(e.target.value)} style={{width:300}}/> - - setReplaceTxt(e.target.value))} style={{width:300}}/> -   - - -
; -} \ No newline at end of file diff --git a/src/App/Components/TwoStateButton.tsx b/src/App/Components/TwoStateButton.tsx deleted file mode 100644 index 60cec2c..0000000 --- a/src/App/Components/TwoStateButton.tsx +++ /dev/null @@ -1,5 +0,0 @@ -import { ButtonHTMLAttributes, PropsWithChildren } from "react"; - -export function TwoStateButton({active, children, className, ...rest}: PropsWithChildren<{active: boolean} & ButtonHTMLAttributes>) { - return -} diff --git a/src/App/Logo/Logo.tsx b/src/App/Logo/Logo.tsx deleted file mode 100644 index 1aa429f..0000000 --- a/src/App/Logo/Logo.tsx +++ /dev/null @@ -1,1578 +0,0 @@ -// i couldn't find a better way to make the text in the logo adapt to light/dark mode... -export function Logo() { - return - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ; -} diff --git a/src/App/Modals/About.tsx b/src/App/Modals/About.tsx index cd0605b..9595c81 100644 --- a/src/App/Modals/About.tsx +++ b/src/App/Modals/About.tsx @@ -1,9 +1,9 @@ -import { Logo } from "@/App/Logo/Logo"; import { Dispatch, ReactElement, SetStateAction } from "react"; +import logo from "../../../artwork/logo-playful.svg"; export function About(props: {setModal: Dispatch>}) { return
-

+

StateBuddy is an open source tool for Statechart editing, simulation, (omniscient) debugging and testing.

diff --git a/src/App/Modals/TextDialog.tsx b/src/App/Modals/TextDialog.tsx index ead2abc..a478877 100644 --- a/src/App/Modals/TextDialog.tsx +++ b/src/App/Modals/TextDialog.tsx @@ -1,20 +1,24 @@ -import { Dispatch, ReactElement, SetStateAction, useState, useCallback } from "react"; +import { Dispatch, ReactElement, SetStateAction, useState, KeyboardEvent, useEffect, useRef } from "react"; import { cachedParseLabel } from "@/statecharts/parser"; -import { useShortcuts } from "@/hooks/useShortcuts"; export function TextDialog(props: {setModal: Dispatch>, text: string, done: (newText: string|undefined) => void}) { const [text, setText] = useState(props.text); - useShortcuts([ - {keys: ["Enter"], action: useCallback(() => { + function onKeyDown(e: KeyboardEvent) { + if (e.key === "Enter") { + if (!e.shiftKey) { + e.preventDefault(); props.done(text); props.setModal(null); - }, [text, props.done, props.setModal])}, - {keys: ["Escape"], action: useCallback(() => { - props.setModal(null); - }, [props.setModal])}, - ], false); + } + } + if (e.key === "Escape") { + props.setModal(null); + e.stopPropagation(); + } + e.stopPropagation(); + } let parseError = ""; try { @@ -24,15 +28,13 @@ export function TextDialog(props: {setModal: Dispatch - {/* Text label:
*/} + return
+ Text label: