diff --git a/global.d.ts b/global.d.ts index 8a65801..946171c 100644 --- a/global.d.ts +++ b/global.d.ts @@ -1,5 +1,4 @@ // without this TypeScript complains when importing CSS files declare module '*.css'; declare module '*.png'; -declare module '*.ttf'; -declare module '*.wav'; \ No newline at end of file +declare module '*.ttf'; \ No newline at end of file diff --git a/src/App/App.tsx b/src/App/App.tsx index 40e952a..f79a9f3 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -21,7 +21,6 @@ import { Plant } from "@/Plant/Plant"; import { usePersistentState } from "@/util/persistent_state"; import { RTHistory } from "./RTHistory"; import { detectConnections } from "@/statecharts/detect_connections"; -import { MicrowavePlant } from "@/Plant/Microwave/Microwave"; export type EditHistory = { current: VisualEditorState, @@ -32,7 +31,6 @@ export type EditHistory = { const plants: [string, Plant][] = [ ["dummy", DummyPlant], ["digital watch", DigitalWatchPlant], - ["microwave", MicrowavePlant], ] export type BigStepError = { @@ -152,6 +150,8 @@ export function App() { const ast = parsed && parsed[0]; const syntaxErrors = parsed && parsed[1]; + console.log('render App', ast); + // append editor state to undo history const makeCheckPoint = useCallback(() => { setEditHistory(historyState => historyState && ({ @@ -278,6 +278,7 @@ export function App() { for (const o of nextConfig.outputEvents) { plantState = plant.reduce(o, plantState); } + console.log({plantState}); newItem = {kind: "bigstep", plantState, ...timedEvent, ...nextConfig}; } catch (error) { @@ -342,6 +343,7 @@ export function App() { } else { const item = current(trace); + console.log(trace); if (item.kind === "bigstep") { highlightActive = item.mode; highlightTransitions = item.firedTransitions; @@ -369,26 +371,31 @@ export function App() { } - {/* top-to-bottom: everything -> bottom panel */}
- - {/* left-to-right: main -> sidebar */}
- {/* top-to-bottom: top bar, editor */} -
- {/* Top bar */} -
- {editHistory && } -
- {/* Editor */} -
- {editorState && conns && syntaxErrors && } + {/* Left: top bar and main editor */} +
+
+ {/* Top bar */} +
+ {editHistory && } +
+ {/* Below the top bar: Editor */} +
+ {editorState && conns && syntaxErrors && } +
@@ -399,7 +406,7 @@ export function App() { flex: '0 0 content', overflowY: "auto", overflowX: "visible", - maxWidth: '50vw', + maxWidth: 'min(300px, 30vw)', }}>
{trace !== null && -
{ - plant.render(trace.trace[trace.idx].plantState, event => onRaise(event.name, event.param)) - }
} + plant.render(trace.trace[trace.idx].plantState, event => onRaise(event.name, event.param))}
setShowExecutionTrace(e.newState === "open")}>execution trace
@@ -462,6 +467,8 @@ export function App() {
+ +
{/* Bottom panel */} diff --git a/src/App/ShowAST.tsx b/src/App/ShowAST.tsx index 1e4b586..2480aa2 100644 --- a/src/App/ShowAST.tsx +++ b/src/App/ShowAST.tsx @@ -1,4 +1,4 @@ -import { ConcreteState, UnstableState, stateDescription, Transition } from "../statecharts/abstract_syntax"; +import { ConcreteState, PseudoState, stateDescription, Transition } from "../statecharts/abstract_syntax"; import { Action, EventTrigger, Expression } from "../statecharts/label_ast"; import { RT_Statechart } from "../statecharts/runtime_types"; @@ -32,7 +32,7 @@ export function ShowAction(props: {action: Action}) { } } -export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | UnstableState}) { +export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | PseudoState}) { const description = stateDescription(props.root); // const outgoing = props.transitions.get(props.root.uid) || []; diff --git a/src/Plant/Microwave/Microwave.css b/src/Plant/Microwave/Microwave.css deleted file mode 100644 index 907b531..0000000 --- a/src/Plant/Microwave/Microwave.css +++ /dev/null @@ -1,14 +0,0 @@ -rect.microwaveButtonHelper { - fill-opacity: 0; -} - -rect.microwaveButtonHelper:hover { - fill: rgba(46, 211, 197); - fill-opacity: 0.5; -} - -rect.microwaveButtonHelper:active { - /* fill: rgba(47, 0, 255); */ - fill: red; - fill-opacity: 0.5; -} diff --git a/src/Plant/Microwave/Microwave.tsx b/src/Plant/Microwave/Microwave.tsx deleted file mode 100644 index 458eb37..0000000 --- a/src/Plant/Microwave/Microwave.tsx +++ /dev/null @@ -1,183 +0,0 @@ -import { preload } from "react-dom"; -import imgSmallClosedOff from "./small_closed_off.png"; -import imgSmallClosedOn from "./small_closed_on.png"; -import imgSmallOpenedOff from "./small_opened_off.png"; -import imgSmallOpenedOn from "./small_opened_off.png"; - -import fontDigital from "../DigitalWatch/digital-font.ttf"; - -import sndBell from "./bell.wav"; -import sndRunning from "./running.wav"; -import { Plant } from "../Plant"; -import { RaisedEvent } from "@/statecharts/runtime_types"; -import { useEffect, useState } from "react"; - -import "./Microwave.css"; - -export type MagnetronState = "on" | "off"; -export type DoorState = "open" | "closed"; - -export function toggleDoor(d: DoorState) { - if (d === "open") { - return "closed"; - } - else return "open"; -} - -export function toggleMagnetron(m: MagnetronState) { - if (m === "on") { - return "off"; - } - return "on"; -} - -export type MicrowaveState = { - // Note: the door state is not part of the MicrowaveState because it is not controlled by the statechart, but by the plant. - timeDisplay: number, - bell: boolean, // whether the bell should ring - magnetron: MagnetronState, -} - -export type MicrowaveProps = { - state: MicrowaveState, - callbacks: { - startPressed: () => void; - stopPressed: () => void; - incTimePressed: () => void; - incTimeReleased: () => void; - doorOpened: () => void; - doorClosed: () => void; - } -} - -const imgs = { - closed: { off: imgSmallClosedOff, on: imgSmallClosedOn }, - open: { off: imgSmallOpenedOff, on: imgSmallOpenedOn }, -} - - -const BUTTON_HEIGHT = 18; -const BUTTON_WIDTH = 60; - -const BUTTON_X0 = 412; -const BUTTON_X1 = BUTTON_X0 + BUTTON_WIDTH; - -const START_X0 = BUTTON_X0; -const START_Y0 = 234; -const START_X1 = BUTTON_X1; -const START_Y1 = START_Y0 + BUTTON_HEIGHT; - -const STOP_X0 = BUTTON_X0; -const STOP_Y0 = 211; -const STOP_X1 = BUTTON_X1; -const STOP_Y1 = STOP_Y0 + BUTTON_HEIGHT; - -const INCTIME_X0 = BUTTON_X0; -const INCTIME_Y0 = 188; -const INCTIME_X1 = BUTTON_X1; -const INCTIME_Y1 = INCTIME_Y0 + BUTTON_HEIGHT; - -const DOOR_X0 = 26; -const DOOR_Y0 = 68; -const DOOR_WIDTH = 353; -const DOOR_HEIGHT = 217; - - -export function Magnetron({state: {timeDisplay, bell, magnetron}, callbacks}: MicrowaveProps) { - const [door, setDoor] = useState("closed"); - const [playBell, setPlayBell] = useState(false); - - // a bit hacky: when the bell-state changes to true, we play the bell sound for 610 ms... - useEffect(() => { - let timeout: NodeJS.Timeout; - if (bell) { - setPlayBell(true); - timeout = setTimeout(() => { - setPlayBell(false); - }, 610); - } - return () => { if (timeout) clearTimeout(timeout); }; - }, [bell]); - - preload(imgSmallClosedOff, {as: "image"}); - preload(imgSmallClosedOn, {as: "image"}); - preload(imgSmallOpenedOff, {as: "image"}); - preload(imgSmallOpenedOn, {as: "image"}); - preload(sndBell, {as: "audio"}); - preload(sndRunning, {as: "audio"}); - - const openDoor = () => { - setDoor("open"); - callbacks.doorOpened(); - } - const closeDoor = () => { - setDoor("closed"); - callbacks.doorClosed(); - } - - return <> - - - - - callbacks.startPressed()} - /> - callbacks.stopPressed()} - /> - callbacks.incTimePressed()} - onMouseUp={() => callbacks.incTimeReleased()} - /> - door === "open" ? closeDoor() : openDoor()} - /> - - {timeDisplay} - - - {magnetron === "on" && } - - {playBell && } - ; -} - -export const MicrowavePlant: Plant = { - inputEvents: [], - outputEvents: [], - initial: { - timeDisplay: 0, - magnetron: "off", - bell: false, - }, - reduce: (inputEvent: RaisedEvent, state: MicrowaveState) => { - if (inputEvent.name === "setMagnetron") { - return { ...state, magnetron: inputEvent.param, bell: false }; - } - if (inputEvent.name === "setTimeDisplay") { - return { ...state, timeDisplay: inputEvent.param, bell: false }; - } - if (inputEvent.name === "ringBell") { - return { ...state, bell: true }; - } - return state; // unknown event - ignore it - }, - render: (state, raiseEvent) => raiseEvent({name: "startPressed"}), - stopPressed: () => raiseEvent({name: "stopPressed"}), - incTimePressed: () => raiseEvent({name: "incTimePressed"}), - incTimeReleased: () => raiseEvent({name: "incTimeReleased"}), - doorOpened: () => raiseEvent({name: "door", param: "open"}), - doorClosed: () => raiseEvent({name: "door", param: "closed"}), - }}/>, -} diff --git a/src/Plant/Microwave/bell.wav b/src/Plant/Microwave/bell.wav deleted file mode 100644 index 3fe70fa..0000000 Binary files a/src/Plant/Microwave/bell.wav and /dev/null differ diff --git a/src/Plant/Microwave/running.wav b/src/Plant/Microwave/running.wav deleted file mode 100644 index ca35830..0000000 Binary files a/src/Plant/Microwave/running.wav and /dev/null differ diff --git a/src/Plant/Microwave/small_closed_off.png b/src/Plant/Microwave/small_closed_off.png deleted file mode 100644 index 3280c99..0000000 Binary files a/src/Plant/Microwave/small_closed_off.png and /dev/null differ diff --git a/src/Plant/Microwave/small_closed_on.png b/src/Plant/Microwave/small_closed_on.png deleted file mode 100644 index 793166f..0000000 Binary files a/src/Plant/Microwave/small_closed_on.png and /dev/null differ diff --git a/src/Plant/Microwave/small_opened_off.png b/src/Plant/Microwave/small_opened_off.png deleted file mode 100644 index 7c829f0..0000000 Binary files a/src/Plant/Microwave/small_opened_off.png and /dev/null differ diff --git a/src/Plant/Microwave/small_opened_on.png b/src/Plant/Microwave/small_opened_on.png deleted file mode 100644 index 6f8708a..0000000 Binary files a/src/Plant/Microwave/small_opened_on.png and /dev/null differ diff --git a/src/VisualEditor/VisualEditor.tsx b/src/VisualEditor/VisualEditor.tsx index b650c58..654a0f8 100644 --- a/src/VisualEditor/VisualEditor.tsx +++ b/src/VisualEditor/VisualEditor.tsx @@ -110,7 +110,7 @@ export const VisualEditor = memo(function VisualEditor({state, setState, trace, x: (e.pageX - bbox.left)/zoom, y: (e.pageY - bbox.top)/zoom, } - }, [refSVG.current, zoom]); + }, [refSVG.current]); const onMouseDown = useCallback((e: {button: number, target: any, pageX: number, pageY: number}) => { const currentPointer = getCurrentPointer(e); diff --git a/src/statecharts/abstract_syntax.ts b/src/statecharts/abstract_syntax.ts index 777e680..2ed2531 100644 --- a/src/statecharts/abstract_syntax.ts +++ b/src/statecharts/abstract_syntax.ts @@ -1,24 +1,20 @@ import { Action, EventTrigger, ParsedText } from "./label_ast"; export type AbstractState = { - kind: string; uid: string; parent?: ConcreteState; - depth: number; comments: [string, string][]; // array of tuple (text-uid, text-text) -} - -export type EntryExitState = AbstractState & { entryActions: Action[]; exitActions: Action[]; + depth: number; } -export type StableState = EntryExitState & { +export type StableState = { kind: "and" | "or"; children: ConcreteState[]; history: HistoryState[]; timers: number[]; // list of timeouts (e.g., the state having an outgoing transition with trigger "after 4s" would appear as the number 4000 in this list) -}; +} & AbstractState; export type AndState = { kind: "and"; @@ -31,24 +27,25 @@ export type OrState = { initial: [string, ConcreteState][]; } & StableState; -export type ConcreteState = AndState | OrState; - -export type TransitionSrcTgt = ConcreteState | UnstableState; - -// also called pseudo-state or choice-state: -export type UnstableState = EntryExitState & { +export type PseudoState = { kind: "pseudo"; -} & AbstractState; + uid: string; + comments: [string, string][]; +}; -export type HistoryState = AbstractState & { +export type HistoryState = { kind: "shallow" | "deep"; + parent: ConcreteState; + uid: string; + depth: number; } +export type ConcreteState = AndState | OrState; export type Transition = { uid: string; // uid of arrow in concrete syntax - src: ConcreteState | UnstableState; - tgt: ConcreteState | UnstableState | HistoryState; + src: ConcreteState | PseudoState; + tgt: ConcreteState | PseudoState | HistoryState; label: ParsedText[]; } @@ -62,7 +59,7 @@ export type Statechart = { internalEvents: EventTrigger[]; outputEvents: Set; - uid2State: Map; + uid2State: Map; historyStates: HistoryState[]; } @@ -113,7 +110,7 @@ export function isOverlapping(a: ConcreteState, b: ConcreteState): boolean { } -export function computeLCA(a: AbstractState, b: AbstractState): AbstractState { +export function computeLCA(a: (ConcreteState|HistoryState), b: (ConcreteState|HistoryState)): (ConcreteState|HistoryState) { if (a === b) { return a; } @@ -123,90 +120,77 @@ export function computeLCA(a: AbstractState, b: AbstractState): AbstractState { return computeLCA(a, b.parent!); } -// arena(a,b) = lowest common or-state ancestor of (a,b) that is not a or b -// see "Deconstructing the Semantics of Big-Step Modelling Languages" by Shahram Esmaeilsabzali, 2009 -export function computeArena(a: AbstractState, b: AbstractState): OrState { - let arena = computeLCA(a, b); - while (arena.kind !== "or" || arena.uid === a.uid || arena.uid === b.uid) { - arena = arena.parent!; +export function computeLCA2(states: (ConcreteState|HistoryState)[]): (ConcreteState|HistoryState) { + if (states.length === 0) { + throw new Error("cannot compute LCA of empty set of states"); } - return arena as OrState; + if (states.length === 1) { + return states[0]; + } + // 2 states or more + return states.reduce((acc, cur) => computeLCA(acc, cur)); } -// export function computeLCA2(states: (ConcreteState|HistoryState)[]): (ConcreteState|HistoryState) { -// if (states.length === 0) { -// throw new Error("cannot compute LCA of empty set of states"); -// } -// if (states.length === 1) { -// return states[0]; -// } -// // 2 states or more -// return states.reduce((acc, cur) => computeLCA(acc, cur)); -// } +export function getPossibleTargets(t: Transition, ts: Map): (ConcreteState|HistoryState)[] { + if (t.tgt.kind !== "pseudo") { + return [t.tgt]; + } + const pseudoOutgoing = ts.get(t.tgt.uid) || []; + return pseudoOutgoing.flatMap(t => getPossibleTargets(t, ts)); +} -// export function getPossibleTargets(t: Transition, ts: Map): (ConcreteState|HistoryState)[] { -// if (t.tgt.kind !== "pseudo") { -// return [t.tgt]; -// } -// const pseudoOutgoing = ts.get(t.tgt.uid) || []; -// return pseudoOutgoing.flatMap(t => getPossibleTargets(t, ts)); -// } - -// export function computeArena2(t: Transition, ts: Map): OrState { -// const tgts = getPossibleTargets(t, ts); -// let lca = computeLCA2([t.src as ConcreteState, ...tgts]); -// while (lca.kind !== "or" || lca === t.src || lca === t.tgt) { -// lca = lca.parent!; -// } -// return lca as OrState; -// } +export function computeArena2(t: Transition, ts: Map): OrState { + const tgts = getPossibleTargets(t, ts); + let lca = computeLCA2([t.src as ConcreteState, ...tgts]); + while (lca.kind !== "or" || lca === t.src || lca === t.tgt) { + lca = lca.parent!; + } + return lca as OrState; +} // Assuming ancestor is already entered, what states to enter in order to enter descendants? // E.g. // root > A > B > C > D // computePath({ancestor: A, descendant: A}) = [] // computePath({ancestor: A, descendant: C}) = [B, C] -export function computePath({ancestor, descendant}: {ancestor: AbstractState, descendant: AbstractState}): AbstractState[] { +export function computePath({ancestor, descendant}: {ancestor: ConcreteState, descendant: (ConcreteState|HistoryState)}): (ConcreteState|HistoryState)[] { if (ancestor === descendant) { return []; } return [...computePath({ancestor, descendant: descendant.parent!}), descendant]; } -// // the arena of a transition is the lowest common ancestor state that is an OR-state -// // see "Deconstructing the Semantics of Big-Step Modelling Languages" by Shahram Esmaeilsabzali, 2009 -// export function computeArena({src, tgt}: {src: ConcreteState, tgt: ConcreteState}): { -// arena: OrState, -// srcPath: ConcreteState[], -// tgtPath: ConcreteState[], -// } { -// if (src.depth >= tgt.depth) { -// const path = isAncestorOf({descendant: src, ancestor: tgt}); -// if (path) { -// if (tgt.kind === "or") { -// return {arena: tgt as OrState, srcPath: path, tgtPath: [tgt]}; -// } -// } -// // keep looking -// const {arena, srcPath, tgtPath} = computeArena({src, tgt: tgt.parent!}); -// return {arena, srcPath, tgtPath: [...tgtPath, tgt]}; -// } -// else { -// // same, but swap src and tgt -// const {arena, srcPath, tgtPath} = computeArena({src: tgt, tgt: src}); -// return {arena, srcPath: tgtPath, tgtPath: srcPath}; -// } -// } +// the arena of a transition is the lowest common ancestor state that is an OR-state +// see "Deconstructing the Semantics of Big-Step Modelling Languages" by Shahram Esmaeilsabzali, 2009 +export function computeArena({src, tgt}: {src: ConcreteState, tgt: ConcreteState}): { + arena: OrState, + srcPath: ConcreteState[], + tgtPath: ConcreteState[], +} { + if (src.depth >= tgt.depth) { + const path = isAncestorOf({descendant: src, ancestor: tgt}); + if (path) { + if (tgt.kind === "or") { + return {arena: tgt as OrState, srcPath: path, tgtPath: [tgt]}; + } + } + // keep looking + const {arena, srcPath, tgtPath} = computeArena({src, tgt: tgt.parent!}); + return {arena, srcPath, tgtPath: [...tgtPath, tgt]}; + } + else { + // same, but swap src and tgt + const {arena, srcPath, tgtPath} = computeArena({src: tgt, tgt: src}); + return {arena, srcPath: tgtPath, tgtPath: srcPath}; + } +} -// transitive, reflexive export function getDescendants(state: ConcreteState): Set { const result = new Set([state.uid]); - if (state.children) { - for (const child of state.children) { - for (const descendant of getDescendants(child)) { - // will include child itself: - result.add(descendant); - } + for (const child of state.children) { + for (const descendant of getDescendants(child)) { + // will include child itself: + result.add(descendant); } } return result; @@ -215,18 +199,17 @@ export function getDescendants(state: ConcreteState): Set { // the 'description' of a state is a human-readable string that (hopefully) identifies the state. // if the state contains a comment, we take the 'first' (= visually topmost) comment // otherwise we fall back to the state's UID. -export function stateDescription(state: AbstractState): string { +export function stateDescription(state: ConcreteState | PseudoState | HistoryState): string { if (state.kind === "shallow") { - return `shallow(${stateDescription(state.parent!)})`; + return `shallow(${stateDescription(state.parent)})`; } else if (state.kind === "deep") { - return `deep(${stateDescription(state.parent!)})`; - } - else if (state.comments.length > 0) { - return state.comments[0][1]; + return `deep(${stateDescription(state.parent)})`; } else { - return state.uid; + // @ts-ignore + const description = state.comments.length > 0 ? state.comments[0][1] : state.uid; + return description; } } diff --git a/src/statecharts/environment.ts b/src/statecharts/environment.ts deleted file mode 100644 index d53dfa2..0000000 --- a/src/statecharts/environment.ts +++ /dev/null @@ -1,102 +0,0 @@ -import { getST, iterST, ScopeTree, updateST, writeST } from "./scope_tree"; - -export type Environment = { - enterScope(scopeId: string): Environment; - exitScope(): Environment; - - // force creation of a new variable in the current scope, even if a variable with the same name already exists in a surrounding scope - newVar(key: string, value: any): Environment; - - // (over)write variable - set(key: string, value: any): Environment; - - // read variable - get(key: string): any; - - entries(): Iterator<[string, any]>; -} - - -// non-hierarchical environment with only global variables -// consistent with the UA MoSIS course on Statecharts -export class FlatEnvironment { - env: ReadonlyMap; - - constructor(env: ReadonlyMap = new Map()) { - this.env = env; - } - - enterScope(scopeId: string): FlatEnvironment { - return this; - } - exitScope(): FlatEnvironment { - return this; - } - - newVar(key: string, value: any) { - return this.set(key, value); - } - set(key: string, value: any) { - return new FlatEnvironment(new Map([...this.env, [key, value]])); - } - get(key: string): any { - return this.env.get(key); - } - - entries(): Iterator<[string, any]> { - return this.env.entries(); - } -} - -// A scoped environment -// IMO better, but harder to explain -export class ScopedEnvironment { - scopeTree: ScopeTree; - current: string[]; - - constructor(scopeTree: ScopeTree = { env: new Map(), children: {} }, current: string[] = []) { - this.scopeTree = scopeTree; - this.current = current; - } - - enterScope(scopeId: string): ScopedEnvironment { - return new ScopedEnvironment( - this.scopeTree, - [...this.current, scopeId], - ); - } - exitScope() { - return new ScopedEnvironment( - this.scopeTree, - this.current.slice(0, -1), - ); - } - - newVar(key: string, value: any): ScopedEnvironment { - return new ScopedEnvironment( - writeST(key, value, this.current, this.scopeTree), - this.current, - ); - } - - // update variable in the innermost scope where it exists, or create it in the current scope if it doesn't exist yet - set(key: string, value: any): ScopedEnvironment { - let updated = updateST(this.current, key, value, this.scopeTree); - if (updated === undefined) { - updated = writeST(key, value, this.current, this.scopeTree); - } - return new ScopedEnvironment( - updated, - this.current, - ) - } - - // lookup variable, starting in the currrent (= innermost) scope, then looking into surrounding scopes until found. - get(key: string): ScopedEnvironment { - return getST(this.current, key, this.scopeTree); - } - - *entries(): Iterator<[string, any]> { - return iterST(this.scopeTree); - } -} diff --git a/src/statecharts/interpreter.ts b/src/statecharts/interpreter.ts index c19faa0..684d81e 100644 --- a/src/statecharts/interpreter.ts +++ b/src/statecharts/interpreter.ts @@ -1,21 +1,16 @@ -import { AbstractState, computeArena, computePath, ConcreteState, getDescendants, HistoryState, isOverlapping, OrState, StableState, Statechart, stateDescription, Transition, transitionDescription, TransitionSrcTgt } from "./abstract_syntax"; +import { computeArena2, computePath, ConcreteState, getDescendants, HistoryState, isOverlapping, OrState, StableState, Statechart, stateDescription, Transition, transitionDescription } from "./abstract_syntax"; import { evalExpr } from "./actionlang_interpreter"; -import { Environment, FlatEnvironment, ScopedEnvironment } from "./environment"; import { Action, EventTrigger, TransitionLabel } from "./label_ast"; -import { BigStepOutput, initialRaised, Mode, RaisedEvents, RT_Event, RT_History, RT_Statechart, TimerElapseEvent, Timers, InputEvent } from "./runtime_types"; - -const initialEnv = new Map([ - ["_timers", []], - ["_log", (str: string) => console.log(str)], -]); -const initialScopedEnvironment = new ScopedEnvironment({env: initialEnv, children: {}}); -// const intiialFlatEnvironment = new FlatEnvironment(initialEnv); +import { BigStepOutput, Environment, initialRaised, Mode, RaisedEvents, RT_Event, RT_History, RT_Statechart, TimerElapseEvent, Timers } from "./runtime_types"; export function initialize(ast: Statechart): BigStepOutput { let history = new Map(); let enteredStates, environment, rest; ({enteredStates, environment, history, ...rest} = enterDefault(0, ast.root, { - environment: initialScopedEnvironment, + environment: new Environment([new Map([ + ["_timers", []], + ["_log", (str: string) => console.log(str)], + ])]), history, ...initialRaised, })); @@ -71,49 +66,42 @@ export function execAction(action: Action, rt: ActionScope): ActionScope { throw new Error("should never reach here"); } -export function entryActions(simtime: number, state: TransitionSrcTgt, actionScope: ActionScope): ActionScope { - console.log('enter', stateDescription(state), '...'); - +export function entryActions(simtime: number, state: ConcreteState, actionScope: ActionScope): ActionScope { + // console.log('enter', stateDescription(state), '...'); let {environment, ...rest} = actionScope; - - environment = environment.enterScope(state.uid); - + // environment = environment.pushScope(); for (const action of state.entryActions) { ({environment, ...rest} = execAction(action, {environment, ...rest})); } // schedule timers - if (state.kind !== "pseudo") { - // we store timers in the environment (dirty!) - const timers: Timers = environment.get("_timers") || []; + // we store timers in the environment (dirty!) + environment = environment.transform("_timers", oldTimers => { const newTimers = [ - ...timers, + ...oldTimers, ...state.timers.map(timeOffset => { const futureSimTime = simtime + timeOffset; return [futureSimTime, {kind: "timer", state: state.uid, timeDurMs: timeOffset}] as [number, TimerElapseEvent]; }), ]; - newTimers.sort((a,b) => a[0] - b[0]); // earliest timers come first - environment = environment.set("_timers", newTimers); - } + newTimers.sort((a,b) => a[0] - b[0]); + return newTimers; + }, []); + // new nested scope return {environment, ...rest}; } -export function exitActions(simtime: number, state: TransitionSrcTgt, {enteredStates, ...actionScope}: EnteredScope): ActionScope { - console.log('exit', stateDescription(state), '...'); - +export function exitActions(simtime: number, state: ConcreteState, {enteredStates, ...actionScope}: EnteredScope): ActionScope { + // console.log('exit', stateDescription(state), '...'); for (const action of state.exitActions) { (actionScope = execAction(action, actionScope)); } let environment = actionScope.environment; // cancel timers - if (state.kind !== "pseudo") { - const timers: Timers = environment.get("_timers") || []; - const newTimers = timers.filter(([_, {state: s}]) => s !== state.uid); - environment = environment.set("_timers", newTimers); - } - - environment = environment.exitScope(); - + environment = environment.transform("_timers", oldTimers => { + // remove all timers of 'state': + return oldTimers.filter(([_, {state: s}]) => s !== state.uid); + }, []); + // environment = environment.popScope(); return {...actionScope, environment}; } @@ -194,37 +182,32 @@ export function enterStates(simtime: number, state: ConcreteState, toEnter: Set< // exit the given state and all its active descendants export function exitCurrent(simtime: number, state: ConcreteState, rt: EnteredScope): ActionScope { - console.log('exitCurrent', stateDescription(state)); let {enteredStates, history, ...actionScope} = rt; if (enteredStates.has(state.uid)) { // exit all active children... - if (state.children) { - for (const child of state.children) { - ({history, ...actionScope} = exitCurrent(simtime, child, {enteredStates, history, ...actionScope})); - } + for (const child of state.children) { + ({history, ...actionScope} = exitCurrent(simtime, child, {enteredStates, history, ...actionScope})); } // execute exit actions ({history, ...actionScope} = exitActions(simtime, state, {enteredStates, history, ...actionScope})); // record history - if (state.history) { - history = new Map(history); // defensive copy - for (const h of state.history) { - if (h.kind === "shallow") { - history.set(h.uid, new Set(state.children - .filter(child => enteredStates.has(child.uid)) - .map(child => child.uid))); - } - else if (h.kind === "deep") { - // horribly inefficient (i don't care) - history.set(h.uid, - getDescendants(state) - .difference(new Set([state.uid])) - .intersection(enteredStates) - ); - } + history = new Map(history); // defensive copy + for (const h of state.history) { + if (h.kind === "shallow") { + history.set(h.uid, new Set(state.children + .filter(child => enteredStates.has(child.uid)) + .map(child => child.uid))); + } + else if (h.kind === "deep") { + // horribly inefficient (i don't care) + history.set(h.uid, + getDescendants(state) + .difference(new Set([state.uid])) + .intersection(enteredStates) + ); } } } @@ -232,106 +215,82 @@ export function exitCurrent(simtime: number, state: ConcreteState, rt: EnteredSc return {history, ...actionScope}; } -function allowedToFire(arena: OrState, alreadyFiredArenas: OrState[]) { - for (const alreadyFired of alreadyFiredArenas) { - if (isOverlapping(arena, alreadyFired)) - return false; - } - return true; -} - -function attemptSrcState(simtime: number, sourceState: AbstractState, event: RT_Event|undefined, statechart: Statechart, {environment, mode, arenasFired, ...rest}: RT_Statechart & RaisedEvents): (RT_Statechart & RaisedEvents) | undefined { - console.log('attemptSrcState', stateDescription(sourceState), arenasFired); - const outgoing = statechart.transitions.get(sourceState.uid) || []; - const labels = outgoing.flatMap(t => - t.label - .filter(l => l.kind === "transitionLabel") - .map(l => [t,l] as [Transition, TransitionLabel])); - let triggered; - if (event !== undefined) { - if (event.kind === "input") { - // get transitions triggered by event - triggered = labels.filter(([_t,l]) => - l.trigger.kind === "event" && l.trigger.event === event.name); - } - else { - // get transitions triggered by timeout - triggered = labels.filter(([_t,l]) => - l.trigger.kind === "after" && l.trigger.durationMs === event.timeDurMs); - } - } - else { - triggered = labels.filter(([_t,l]) => l.trigger.kind === "triggerless"); - } - // eval guard - const inState = (stateLabel: string) => { - for (const [uid, state] of statechart.uid2State.entries()) { - if (stateDescription(state) === stateLabel) { - return (mode.has(uid)); - } - } - }; - const guardEnvironment = environment.set("inState", inState); - const enabled = triggered.filter(([t,l]) => evalExpr(l.guard, guardEnvironment)); - if (enabled.length > 0) { - if (enabled.length > 1) { - throw new NonDeterminismError(`Non-determinism: state '${stateDescription(sourceState)}' has multiple (${enabled.length}) enabled outgoing transitions: ${enabled.map(([t]) => transitionDescription(t)).join(', ')}`, [...enabled.map(([t]) => t.uid), sourceState.uid]); - } - const [toFire, label] = enabled[0]; - const arena = computeArena(toFire.src, toFire.tgt); - if (allowedToFire(arena, arenasFired)) { - environment = environment.enterScope(""); - // if there's an event parameter, add it to environment - if (event && event.kind === "input" && event.param !== undefined) { - const varName = (label.trigger as EventTrigger).paramName as string; - environment = environment.set(varName, event.param); - } - ({mode, environment, ...rest} = fire(simtime, toFire, statechart.transitions, label, arena, {mode, environment, ...rest})); - rest = {...rest, firedTransitions: [...rest.firedTransitions, toFire.uid]} - environment.exitScope(); - arenasFired = [...arenasFired, arena]; - - // if there is any pseudo-state in the modal configuration, immediately fire any enabled outgoing transitions of that state: - for (const activeState of mode) { - const s = statechart.uid2State.get(activeState); - if (s?.kind === "pseudo") { - console.log('fire pseudo-state...'); - const newConfig = attemptSrcState(simtime, s, undefined, statechart, {environment, mode, arenasFired: [], ...rest}); - if (newConfig === undefined) { - throw new RuntimeError("Stuck in choice-state.", [activeState]); - } - arenasFired = [...arenasFired, ...newConfig.arenasFired]; - return {...newConfig, arenasFired}; - } - } - return {mode, environment, arenasFired, ...rest}; - } - } -} - -// A fair step is a response to one (input|internal) event, where possibly multiple transitions are made as long as their arenas do not overlap. A reasonably accurate and more intuitive explanation is that every orthogonal region is allowed to fire at most one transition. -export function fairStep(simtime: number, event: RT_Event, statechart: Statechart, activeParent: StableState, {arenasFired, ...config}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { - console.log('fairStep', arenasFired); +export function handleEvent(simtime: number, event: RT_Event, statechart: Statechart, activeParent: StableState, {environment, mode, ...rest}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { + const arenasFired = new Set(); for (const state of activeParent.children) { - if (config.mode.has(state.uid)) { - const didFire = attemptSrcState(simtime, state, event, statechart, {...config, arenasFired}); - if (didFire) { - ({arenasFired, ...config} = didFire); + if (mode.has(state.uid)) { + const outgoing = statechart.transitions.get(state.uid) || []; + const labels = outgoing.flatMap(t => + t.label + .filter(l => l.kind === "transitionLabel") + .map(l => [t,l] as [Transition, TransitionLabel])); + let triggered; + if (event.kind === "input") { + // get transitions triggered by event + triggered = labels.filter(([_t,l]) => + l.trigger.kind === "event" && l.trigger.event === event.name); + } + else { + // get transitions triggered by timeout + triggered = labels.filter(([_t,l]) => + l.trigger.kind === "after" && l.trigger.durationMs === event.timeDurMs); + } + // eval guard + const guardEnvironment = environment.set("inState", (stateLabel: string) => { + for (const [uid, state] of statechart.uid2State.entries()) { + if (stateDescription(state) === stateLabel) { + return (mode.has(uid)); + } + } + }); + const enabled = triggered.filter(([t,l]) => + evalExpr(l.guard, guardEnvironment)); + if (enabled.length > 0) { + if (enabled.length > 1) { + throw new NonDeterminismError(`Non-determinism: state '${stateDescription(state)}' has multiple (${enabled.length}) enabled outgoing transitions: ${enabled.map(([t]) => transitionDescription(t)).join(', ')}`, [...enabled.map(([t]) => t.uid), state.uid]); + } + const [t,l] = enabled[0]; // just pick one transition + const arena = computeArena2(t, statechart.transitions); + let overlapping = false; + for (const alreadyFired of arenasFired) { + if (isOverlapping(arena, alreadyFired)) { + overlapping = true; + } + } + if (!overlapping) { + if (event.kind === "input" && event.param !== undefined) { + // input events may have a parameter + // add event parameter to environment in new scope + environment = environment.pushScope(); + environment = environment.newVar( + (l.trigger as EventTrigger).paramName as string, + event.param, + ); + } + ({mode, environment, ...rest} = fireTransition(simtime, t, statechart.transitions, l, arena, {mode, environment, ...rest})); + if (event.kind === "input" && event.param !== undefined) { + environment = environment.popScope(); + } + arenasFired.add(arena); + } + else { + // console.log('skip (overlapping arenas)'); + } } else { // no enabled outgoing transitions, try the children: - console.log('attempt children'); - ({arenasFired, ...config} = fairStep(simtime, event, statechart, state, {...config, arenasFired})); + ({environment, mode, ...rest} = handleEvent(simtime, event, statechart, state, + {environment, mode, ...rest})); } } } - return {arenasFired, ...config}; + return {environment, mode, ...rest}; } export function handleInputEvent(simtime: number, event: RT_Event, statechart: Statechart, {mode, environment, history}: {mode: Mode, environment: Environment, history: RT_History}): BigStepOutput { let raised = initialRaised; - ({mode, environment, ...raised} = fairStep(simtime, event, statechart, statechart.root, {mode, environment, history, arenasFired: [], ...raised})); + ({mode, environment, ...raised} = handleEvent(simtime, event, statechart, statechart.root, {mode, environment, history, ...raised})); return handleInternalEvents(simtime, statechart, {mode, environment, history, ...raised}); } @@ -339,127 +298,77 @@ export function handleInputEvent(simtime: number, event: RT_Event, statechart: S export function handleInternalEvents(simtime: number, statechart: Statechart, {internalEvents, ...rest}: RT_Statechart & RaisedEvents): BigStepOutput { while (internalEvents.length > 0) { const [nextEvent, ...remainingEvents] = internalEvents; - ({internalEvents, ...rest} = fairStep(simtime, + ({internalEvents, ...rest} = handleEvent(simtime, {kind: "input", ...nextEvent}, // internal event becomes input event - statechart, statechart.root, { arenasFired: [], internalEvents: remainingEvents, ...rest})); + statechart, statechart.root, {internalEvents: remainingEvents, ...rest})); } return rest; } -function resolveHistory(tgt: AbstractState, history: RT_History): Set { - if (tgt.kind === "shallow" || tgt.kind === "deep") { - const toEnter = history.get(tgt.uid) || new Set(); - return toEnter; - } - else { - const toEnter = new Set([tgt.uid]); - return toEnter; - } -} +export function fireTransition(simtime: number, t: Transition, ts: Map, label: TransitionLabel, arena: OrState, {mode, environment, history, ...rest}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { + console.log('fire', transitionDescription(t)); -export function fire(simtime: number, t: Transition, ts: Map, label: TransitionLabel, arena: OrState, {mode, environment, history, ...rest}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { - console.log('will now fire', transitionDescription(t), 'arena', arena); + const srcPath = computePath({ancestor: arena, descendant: t.src as ConcreteState}).reverse() as ConcreteState[]; - const srcPath = computePath({ancestor: arena, descendant: t.src as ConcreteState}) as ConcreteState[]; - - console.log(srcPath); // console.log('arena:', arena, 'srcPath:', srcPath); // exit src and other states up to arena - ({environment, history, ...rest} = exitCurrent(simtime, srcPath[0], {environment, enteredStates: mode, history, ...rest})); + ({environment, history, ...rest} = exitCurrent(simtime, srcPath[0], {environment, enteredStates: mode, history, ...rest})) const toExit = getDescendants(arena); toExit.delete(arena.uid); // do not exit the arena itself - const exitedMode = mode.difference(toExit); // active states after exiting + const exitedMode = mode.difference(toExit); // active states after exiting the states we need to exit - console.log('toExit', toExit); - console.log('exitedMode', exitedMode); + // console.log({exitedMode}); - // transition actions - for (const action of label.actions) { - ({environment, history, ...rest} = execAction(action, {environment, history, ...rest})); - } - - const tgtPath = computePath({ancestor: arena, descendant: t.tgt}); - const state = tgtPath[0] as ConcreteState; // first state to enter - const toEnter = resolveHistory(t.tgt, history) - .union(new Set(tgtPath.map(s=>s.uid))); - - let enteredStates; - ({enteredStates, environment, history, ...rest} = enterStates(simtime, state, toEnter, {environment, history, ...rest})); - const enteredMode = exitedMode.union(enteredStates); - - console.log('new mode', enteredMode); - - console.log('done firing', transitionDescription(t)); - - return {mode: enteredMode, environment, history, ...rest}; + return fireSecondHalfOfTransition(simtime, t, ts, label, arena, {mode: exitedMode, history, environment, ...rest}); } -// export function fireTransition(simtime: number, t: Transition, ts: Map, label: TransitionLabel, arena: OrState, {mode, environment, history, ...rest}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { -// console.log('fire', transitionDescription(t)); +// assuming we've already exited the source state of the transition, now enter the target state +// IF however, the target is a pseudo-state, DON'T enter it (pseudo-states are NOT states), instead fire the first pseudo-outgoing transition. +export function fireSecondHalfOfTransition(simtime: number, t: Transition, ts: Map, label: TransitionLabel, arena: OrState, {mode, environment, history, firedTransitions, ...raised}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { + // exec transition actions + for (const action of label.actions) { + ({environment, history, firedTransitions, ...raised} = execAction(action, {environment, history, firedTransitions, ...raised})); + } -// const srcPath = computePath({ancestor: arena, descendant: t.src as ConcreteState}).reverse() as ConcreteState[]; + firedTransitions = [...firedTransitions, t.uid]; -// // console.log('arena:', arena, 'srcPath:', srcPath); - -// // exit src and other states up to arena -// ({environment, history, ...rest} = exitCurrent(simtime, srcPath[0], {environment, enteredStates: mode, history, ...rest})) -// const toExit = getDescendants(arena); -// toExit.delete(arena.uid); // do not exit the arena itself -// const exitedMode = mode.difference(toExit); // active states after exiting the states we need to exit - -// // console.log({exitedMode}); - -// return fireSecondHalfOfTransition(simtime, t, ts, label, arena, {mode: exitedMode, history, environment, ...rest}); -// } - -// // assuming we've already exited the source state of the transition, now enter the target state -// // IF however, the target is a pseudo-state, DON'T enter it (pseudo-states are NOT states), instead fire the first pseudo-outgoing transition. -// export function fireSecondHalfOfTransition(simtime: number, t: Transition, ts: Map, label: TransitionLabel, arena: OrState, {mode, environment, history, firedTransitions, ...raised}: RT_Statechart & RaisedEvents): RT_Statechart & RaisedEvents { -// console.log('fire (2nd half)', transitionDescription(t)); -// // exec transition actions -// for (const action of label.actions) { -// ({environment, history, firedTransitions, ...raised} = execAction(action, {environment, history, firedTransitions, ...raised})); -// } - -// firedTransitions = [...firedTransitions, t.uid]; - -// if (t.tgt.kind === "pseudo") { -// const outgoing = ts.get(t.tgt.uid) || []; -// for (const nextT of outgoing) { -// for (const nextLabel of nextT.label) { -// if (nextLabel.kind === "transitionLabel") { -// if (evalExpr(nextLabel.guard, environment)) { -// console.log('fire', transitionDescription(nextT)); -// // found ourselves an enabled transition -// return fireSecondHalfOfTransition(simtime, nextT, ts, nextLabel, arena, {mode, environment, history, firedTransitions, ...raised}); -// } -// } -// } -// } -// throw new Error("stuck in pseudo-state!!"); -// } -// else { -// const tgtPath = computePath({ancestor: arena, descendant: t.tgt}); -// const state = tgtPath[0] as ConcreteState; -// let toEnter; -// if (t.tgt.kind === "deep" || t.tgt.kind === "shallow") { -// toEnter = new Set([ -// ...tgtPath.slice(0,-1).map(s => s.uid), -// ...history.get(t.tgt.uid)! -// ]) as Set; -// } -// else { -// toEnter = new Set(tgtPath.map(s=>s.uid)); -// } + if (t.tgt.kind === "pseudo") { + const outgoing = ts.get(t.tgt.uid) || []; + for (const nextT of outgoing) { + for (const nextLabel of nextT.label) { + if (nextLabel.kind === "transitionLabel") { + if (evalExpr(nextLabel.guard, environment)) { + console.log('fire', transitionDescription(nextT)); + // found ourselves an enabled transition + return fireSecondHalfOfTransition(simtime, nextT, ts, nextLabel, arena, {mode, environment, history, firedTransitions, ...raised}); + } + } + } + } + throw new Error("stuck in pseudo-state!!"); + } + else { + const tgtPath = computePath({ancestor: arena, descendant: t.tgt}); + const state = tgtPath[0] as ConcreteState; + let toEnter; + if (t.tgt.kind === "deep" || t.tgt.kind === "shallow") { + toEnter = new Set([ + ...tgtPath.slice(0,-1).map(s => s.uid), + ...history.get(t.tgt.uid)! + ]) as Set; + } + else { + toEnter = new Set(tgtPath.map(s=>s.uid)); + } -// // enter tgt -// let enteredStates; -// ({enteredStates, environment, history, firedTransitions, ...raised} = enterStates(simtime, state, toEnter, {environment, history, firedTransitions, ...raised})); -// const enteredMode = mode.union(enteredStates); + // enter tgt + let enteredStates; + ({enteredStates, environment, history, firedTransitions, ...raised} = enterStates(simtime, state, toEnter, {environment, history, firedTransitions, ...raised})); + const enteredMode = mode.union(enteredStates); -// // console.log({enteredMode}); + // console.log({enteredMode}); -// return {mode: enteredMode, environment, history, firedTransitions, ...raised}; -// } -// } + return {mode: enteredMode, environment, history, firedTransitions, ...raised}; + } +} diff --git a/src/statecharts/mtl/ast.ts b/src/statecharts/mtl/ast.ts deleted file mode 100644 index 72d6432..0000000 --- a/src/statecharts/mtl/ast.ts +++ /dev/null @@ -1,247 +0,0 @@ -import { _evolve } from "./helpers"; - -type MTL_Node = any; - -function flatten_binary(phi: NaryOpMTL, op, dropT, shortT) { - const args = phi.args.filter(arg => arg !== dropT); - - if (args.some((arg: MTL_Node) => arg === shortT)) { - return shortT; - } - if (args.length === 0) { - return dropT; - } - if (args.length === 1) { - return args[0]; - } - - function f(x) { - if (x instanceof op) { - return x.args; - } - else { - return [x]; - } - } - - return op(phi.args.flatMap(f)) -} - -function _neg(expr: MTL_Node) { - if (expr instanceof Neg) { - return expr.arg; - } - return new Neg(expr); -} - -function _and(expr1: MTL_Node, expr2: MTL_Node) { - return flatten_binary(new And([expr1, expr2]), And, TOP, BOT); -} - -function _or(expr1: MTL_Node, expr2: MTL_Node) { - return _neg(_and(_neg(expr1), _neg(expr2))) -} - -function _eval(expr, trace, time=false, dt=0.1, quantitative=true) { - return evaluator.pointwise_sat(expr, dt)(trace, time, quantitative); -} - -function _timeshift(expr, t) { - if (expr === BOT) { - return expr; - } - for (let i=0; i 0) { - const node = children.pop(); - yield node; - children.push(...node.children); - } -} - -function _params(expr) { - function* get_params(leaf) { - if (leaf.interval[0] instanceof Param) { - yield leaf.interval[0]; - } - if (leaf.interval[1] instanceof Param) { - yield leaf.interval[1]; - } - } - - return new Set(_walk(expr).flatMap(e => [...get_params(e)])); -} - -function _set_symbols(node, val) { - const children = (node.children?.() || []).map(c => _set_symbols(c, val)); - - if (node.interval) { - return _evolve(node, { - arg: children[0], - interval: _update_itvl(node.interval, val), - }); - } - if (node instanceof AtomicPred) { - return val.get(node.id, node); - } - if (node.args) { - return _evolve(node, { - args: children, - }); - } - if (node.arg) { - return _evolve(node, { - args: children, - }); - } - return node; -} - -function _update_itvl(itvl, lookup) { - function _update_param(p) { - if (!(p instanceof Param) || !lookup.has(p.name)) { - return p; - } - const val = lookup.get(p.name); - if (lookup instanceof Param) { - return val; - } - else { - return Number(val); - } - } - - return new Interval(_update_param(itvl.lower), _update_param(itvl.upper)); -} - - -function alw(phi: MTL_Node, lo=0, hi=Infinity) { - return new G(new Interval(lo, hi), phi); -} - -function env(phi: MTL_Node, lo=0, hi=Infinity) { - return ~alw(~phi, lo, hi); -} - -function implies(x, y) { - return _neg(x) -} - - - -class AtomicPred { - id: string; - - constructor(id: string) { - this.id = id; - } -} - -class Interval { - lower: number | Param; - upper: number | Param; - - constructor(lower: number | Param, uppper: number | Param) { - this.lower = lower; - this.upper = uppper; - } -} - -class Param { - name: string; - - constructor(name: string) { - this.name = name; - } -} - -class _Bot {} - -class NaryOpMTL { - OP = "?"; - args: MTL_Node[]; - - constructor(args: MTL_Node[]) { - this.args = args; - } - - children() { - return this.args; - } -} - -class And extends NaryOpMTL { - OP = "&"; -} - -class ModalOp { - OP = "?"; - interval: Interval; - arg: MTL_Node - - constructor(interval: Interval, arg: MTL_Node) { - this.interval = interval; - this.arg = arg; - } - - children() { - return [this.arg]; - } -} - -class G extends ModalOp { - OP = "G"; -} - -class WeakUntil { - arg1: MTL_Node; - arg2: MTL_Node; - - constructor(arg1: MTL_Node, arg2: MTL_Node) { - this.arg1 = arg1; - this.arg2 = arg2; - } - - children() { - return [this.arg1, this.arg2]; - } -} - -class Neg { - arg: MTL_Node; - - constructor(arg: MTL_Node) { - this.arg = arg; - } - - children() { - return [this.arg]; - } -} - -class Next { - arg: MTL_Node - - constructor(arg: MTL_Node) { - this.arg = arg; - } - - - children() { - return [this.arg]; - } -} - -function type_pred(...args) { - const ast_types = new Set(args); - return (x: any) => ast_types.has(x.constructor); -} - -export const BOT = new _Bot(); -export const TOP = _neg(BOT); \ No newline at end of file diff --git a/src/statecharts/mtl/evaluator.ts b/src/statecharts/mtl/evaluator.ts deleted file mode 100644 index 5ae2e79..0000000 --- a/src/statecharts/mtl/evaluator.ts +++ /dev/null @@ -1,50 +0,0 @@ -import { BOT, TOP } from "./ast"; -import { DiscreteSignal, signal } from "./signals"; - -const CONST_FALSE = signal([[0,-1]], -Infinity, Infinity, BOT); -const CONST_TRUE = signal([[0, 1]], -Infinity, Infinity, TOP); - -export function eval_mtl_until(phi, dt) { - -} - -export function eval_mtl_g(phi, dt) { - const f = eval_mtl(phi.arg, dt); - const [a,b] = phi.interval; - if (b < a) { - return _ => CONST_TRUE.retag(new Map([[TOP, phi]])); - } - function _min(val) { - return Math.min(...val[phi.arg]); - } - return x => { - let tmp: DiscreteSignal = f(x); - if (b < a) throw new Error("assertion failed"); - if (b > a) { - if (b < Infinity) { - const ts = tmp.times().map(t => interp_all(tmp, t-b-a+dt, tmp.end)); - tmp = ts.reduce((a,b) => a.__or__(b), tmp).slice(tmp.start, tmp.end); - } - return tmp.rolling(a,b).map(_min, phi); - } - return tmp.retag(new Map([[phi.arg, phi]])); - } -} - -export function eval_mtl_neg(phi, dt) { - const f = eval_mtl(phi.arg, dt); - return x => f(x).map(v => -v[phi.arg], phi); -} - -export function eval_mtl_next(phi, dt) { - const f = eval_mtl(phi.arg, dt); - return x => f(x).lshift(dt).retag(new Map([[phi.arg, phi]])); -} - -export function eval_mtl_ap(phi, _) { - return (x: DiscreteSignal) => x.project(new Set([phi.id]).retag(new Map([[phi.id, phi]]))); -} - -export function eval_mtl_bot(_, _1) { - return () => CONST_FALSE -} diff --git a/src/statecharts/mtl/helpers.ts b/src/statecharts/mtl/helpers.ts deleted file mode 100644 index 924528a..0000000 --- a/src/statecharts/mtl/helpers.ts +++ /dev/null @@ -1,9 +0,0 @@ - -export function _evolve(object, changes) { - return Object.assign( - Object.create(Object.getPrototypeOf(object)), // create empty object with same prototype as original - { - ...object, - ...changes, - }); -} diff --git a/src/statecharts/mtl/signals.ts b/src/statecharts/mtl/signals.ts deleted file mode 100644 index 7b58f6c..0000000 --- a/src/statecharts/mtl/signals.ts +++ /dev/null @@ -1,149 +0,0 @@ -// Ported from https://github.com/mvcisback/DiscreteSignals/blob/main/discrete_signals/signals.py - -import { _evolve } from "./helpers"; - - -type Time = number; -type KeyType = any; -type ValueType = any; -type DataType = Map>; - -export class DiscreteSignal { - data: DataType; - start: Time; - end: Time; - - constructor(data: DataType, start: Time, end: Time) { - this.data = data; - this.start = start; - this.end = end; - } - - values() { - return this.data.values(); - } - times() { - return this.data.keys(); - } - entries() { - return this.data.entries(); - } - - tags() { - return new Set([].concat(...[...this.values()])); - } - - rshift(delta: Time) { - return _evolve(this, - { - data: new Map(...this.data.entries().map(([time, val]) => [time+delta, val] as [Time, any])), - start: this.start + delta, - end: this.end + delta, - } - ) - } - - lshift(delta: Time) { - return this.rshift(-delta); - } - - matmul(other) { - return _evolve(this, - { - data: new Map([ - ...this.data.entries(), - ...other.data.entries().map(([time, val]) => [time+this.end, val]), - ]), - end: this.end + (other.end - other.start), - } - ) - } - - __or__(other) { - return _evolve(this, - { - // merge all data: - data: new Map([...new Set([...this.data.keys(), ...other.data.keys()])].map(key => [key, new Map([ - ...this.data.get(key)?.entries() || [], - ...other.data.get(key)?.entries() || [], - ])])), - start: Math.min(this.start, other.start), - end: Math.max(this.end, other.end), - } - ) - } - - slice(start?: number, end?: number) { - const s = (start === undefined) ? this.start : start; - const e = (end === undefined) ? this.end : end; - return _evolve(this, { - data: new Map([...this.data.entries().filter(([time]) => time >= s && time < e)]), - start: s, - end: e, - }) - } - - get(key: number) { - return this.data.get(key); - } - - rolling(start: number, end: number) { - if (start !== 0) { - const delta = (end !== Infinity) ? (end - start) : end - return this.rolling(0, delta).lshift(start); - } - - const apply_window = ([t, _]) => { - const values = this.slice(start+t, end+t).values(); - return [t, values]; - } - - return _evolve(this, { - data: new Map([...this.data.entries().map((entry) => apply_window(entry))]), - end: (end < this.end) ? (this.end - end) : this.end, - }) - } - - transform(f: (val: Map) => Map) { - const data = new Map([ - ...this.data.entries().map(([key, val]) => - [key, f(val)] as [Time, any])]); - return _evolve(this, { - data, - }); - } - - map(f: (val: Map) => Map, tag=null) { - const data = new Map([ - ...this.data.entries().map(([key, val]) => - [key, f(val)] as [Time, any])]); - return signal(data, this.start, this.end, tag); - } - - - filter(f: (val: Map) => boolean) { - return _evolve(this, { - data: new Map([...this.data.entries().filter(([_, val]) => f(val))]), - }); - } - - project(keys: Set) { - return this - .transform(val => new Map([...val.entries()].filter(([key]) => keys.has(key)))) - .filter(val => keys.intersection(val.keys()).size > 0); - } - - retag(mapping: Map) { - return this.transform(val => - new Map([...val.entries().map(([key,val]) => - [mapping.get(key), val] as [KeyType, ValueType])])); - } -} - -export function signal(data: Iterable<[number, number]>, start=0, end=Infinity, tag:any = 'null') { - return new DiscreteSignal( - new Map([...data].map(([time, value]) => [time, new Map([[tag, value]])])), - start, - end - ).slice(start, end); -} diff --git a/src/statecharts/parser.ts b/src/statecharts/parser.ts index a7d1862..d53388a 100644 --- a/src/statecharts/parser.ts +++ b/src/statecharts/parser.ts @@ -1,4 +1,4 @@ -import { ConcreteState, HistoryState, OrState, UnstableState, Statechart, stateDescription, Transition } from "./abstract_syntax"; +import { ConcreteState, HistoryState, OrState, PseudoState, Statechart, stateDescription, Transition } from "./abstract_syntax"; import { Rountangle } from "./concrete_syntax"; import { isEntirelyWithin, Rect2D } from "../VisualEditor/geometry"; import { Action, EventTrigger, Expression, ParsedText } from "./label_ast"; @@ -51,7 +51,7 @@ export function parseStatechart(state: VisualEditorState, conns: Connections): [ timers: [], } - const uid2State = new Map([["root", root]]); + const uid2State = new Map([["root", root]]); const historyStates: HistoryState[] = []; // we will always look for the smallest parent rountangle @@ -116,18 +116,11 @@ export function parseStatechart(state: VisualEditorState, conns: Connections): [ uid2State.set(rt.uid, state as ConcreteState); } for (const d of state.diamonds) { - const parent = findParent(d); - const pseudoState = { + uid2State.set(d.uid, { kind: "pseudo", uid: d.uid, comments: [], - depth: parent.depth+1, - parent, - entryActions: [], - exitActions: [], - }; - uid2State.set(d.uid, pseudoState); - parent.children.push(pseudoState); + }); } for (const h of state.history) { const parent = findParent({topLeft: h.topLeft, size: {x: HISTORY_RADIUS*2, y: HISTORY_RADIUS*2}}); diff --git a/src/statecharts/runtime_types.ts b/src/statecharts/runtime_types.ts index 3d65d4a..ec99da9 100644 --- a/src/statecharts/runtime_types.ts +++ b/src/statecharts/runtime_types.ts @@ -1,5 +1,3 @@ -import { Environment } from "./environment"; - export type Timestamp = number; // milliseconds since begin of simulation export type RT_Event = InputEvent | TimerElapseEvent; @@ -19,6 +17,80 @@ export type TimerElapseEvent = { export type Mode = Set; // set of active states +export class Environment { + scopes: ReadonlyMap[]; // array of nested scopes - scope at the back of the array is used first + + constructor(env = [new Map()] as ReadonlyMap[]) { + this.scopes = env; + } + + pushScope(): Environment { + return new Environment([...this.scopes, new Map()]); + } + + popScope(): Environment { + return new Environment(this.scopes.slice(0, -1)); + } + + // force creation of a new variable in the current scope, even if a variable with the same name already exists in a surrounding scope + newVar(key: string, value: any): Environment { + return new Environment( + this.scopes.with( + this.scopes.length-1, + new Map([ + ...this.scopes[this.scopes.length-1], + [key, value], + ]), + )); + } + + // update variable in the innermost scope where it exists, or create it in the current scope if it doesn't exist yet + set(key: string, value: any): Environment { + for (let i=this.scopes.length-1; i>=0; i--) { + const map = this.scopes[i]; + if (map.has(key)) { + return new Environment(this.scopes.with(i, new Map([ + ...map.entries(), + [key, value], + ]))); + } + } + return new Environment(this.scopes.with(-1, new Map([ + ...this.scopes[this.scopes.length-1].entries(), + [key, value], + ]))); + } + + // lookup variable, starting in the currrent (= innermost) scope, then looking into surrounding scopes until found. + get(key: string): any { + for (let i=this.scopes.length-1; i>=0; i--) { + const map = this.scopes[i]; + const found = map.get(key); + if (found !== undefined) { + return found; + } + } + } + + transform(key: string, upd: (old:T) => T, defaultVal: T): Environment { + const old = this.get(key) || defaultVal; + return this.set(key, upd(old)); + } + + *entries() { + const visited = new Set(); + for (let i=this.scopes.length-1; i>=0; i--) { + const map = this.scopes[i]; + for (const [key, value] of map.entries()) { + if (!visited.has(key)) { + yield [key, value]; + visited.add(key); + } + } + } + } +} + export type RT_History = Map>; export type RT_Statechart = { diff --git a/src/statecharts/scope_tree.ts b/src/statecharts/scope_tree.ts deleted file mode 100644 index 3a06076..0000000 --- a/src/statecharts/scope_tree.ts +++ /dev/null @@ -1,88 +0,0 @@ -export type ScopeTree = { - env: ReadonlyMap; - children: { [key: string]: ScopeTree }; -} - -// create or update an entry somewhere in the scope tree -export function writeST(key: string, val: any, path: string[], {env, children}: ScopeTree): ScopeTree { - if (path.length === 0) { - return { - env: new Map([...env, [key, val]]), - children, - }; - } - else { - const [childId, ...rest] = path; - return { - env, - children: { - ...children, - [childId]: writeST(key, val, rest, children[childId] || {env: new Map(), children: {}}), - }, - }; - } -} - -export function getST(path: string[], key: string, {env, children}: ScopeTree): any | undefined { - if (path.length === 0) { - if (env.has(key)) { - return env.get(key); - } - return; // not found - } - else { - // follow path - const [childId, ...rest] = path; - let found; - if (Object.hasOwn(children, childId)) { - found = getST(rest, key, children[childId]); - } - if (found === undefined) { - // lookup in parent (yes that's us) - return getST([], key, {env, children}); - } - else { - return found; - } - } -} - -// only overwrites variable if it exists somewhere along the path, preferring deep over shallow -// otherwise, returns undefined. -export function updateST(path: string[], key: string, val: any, {env, children}: ScopeTree): ScopeTree | undefined { - if (path.length === 0) { - if (env.has(key)) { - return { env: new Map([...env, [key, val]]), children }; - } - return; - } - else { - // follow path - const [childId, ...rest] = path; - let updated; - if (Object.hasOwn(children, childId)) { - updated = updateST(rest, key, val, children[childId]); - } - if (updated === undefined) { - // attempt overwrite in parent (yes that's us) - return updateST([], key, val, {env, children}); - } - else { - return { - env, - children: { ...children, [childId]: updated }, - } - } - } -} - -export function* iterST({env, children}: ScopeTree): IterableIterator<[string, any]> { - for (const [key, val] of env) { - yield [key, val]; - } - for (const [childId, child] of Object.entries(children)) { - for (const [key, val] of iterST(child)) { - yield [childId+'.'+key, val]; - } - } -} diff --git a/todo.txt b/todo.txt index a82e787..73444e0 100644 --- a/todo.txt +++ b/todo.txt @@ -27,9 +27,6 @@ TODO -- bugs - interpreter: pseudo-state semantics is broken - - testing use STL for testing https://github.com/mvcisback/py-metric-temporal-logic @@ -39,18 +36,11 @@ TODO - outgoing transitions? - usability stuff: - - action language: add increment operations (++) and (--) - and (+=) and (-=) - - - snap: - comments only to states - triggers only to transitions - entry/exit only to states - - ability to hide statechart and only show the plant? - hovering over event in side panel should highlight all occurrences of the event in the SC - hovering over error in bottom panel should highlight that rror in the SC - highlight selected shapes while making a selection + - comments sometimes snap to transitions even if they belong to a state - highlight fired transitions - highlight about-to-fire transitions