diff --git a/global.d.ts b/global.d.ts index 946171c..8a65801 100644 --- a/global.d.ts +++ b/global.d.ts @@ -1,4 +1,5 @@ // without this TypeScript complains when importing CSS files declare module '*.css'; declare module '*.png'; -declare module '*.ttf'; \ No newline at end of file +declare module '*.ttf'; +declare module '*.wav'; \ No newline at end of file diff --git a/src/App/App.tsx b/src/App/App.tsx index f79a9f3..40e952a 100644 --- a/src/App/App.tsx +++ b/src/App/App.tsx @@ -21,6 +21,7 @@ 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, @@ -31,6 +32,7 @@ export type EditHistory = { const plants: [string, Plant][] = [ ["dummy", DummyPlant], ["digital watch", DigitalWatchPlant], + ["microwave", MicrowavePlant], ] export type BigStepError = { @@ -150,8 +152,6 @@ 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,7 +278,6 @@ 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) { @@ -343,7 +342,6 @@ export function App() { } else { const item = current(trace); - console.log(trace); if (item.kind === "bigstep") { highlightActive = item.mode; highlightTransitions = item.firedTransitions; @@ -371,31 +369,26 @@ export function App() { } + {/* top-to-bottom: everything -> bottom panel */}
+ + {/* left-to-right: main -> sidebar */}
- {/* Left: top bar and main editor */} -
-
- {/* Top bar */} -
- {editHistory && } -
- {/* Below the top bar: Editor */} -
- {editorState && conns && syntaxErrors && } -
+ {/* top-to-bottom: top bar, editor */} +
+ {/* Top bar */} +
+ {editHistory && } +
+ {/* Editor */} +
+ {editorState && conns && syntaxErrors && }
@@ -406,7 +399,7 @@ export function App() { flex: '0 0 content', overflowY: "auto", overflowX: "visible", - maxWidth: 'min(300px, 30vw)', + maxWidth: '50vw', }}>
{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
@@ -467,8 +462,6 @@ export function App() {
- -
{/* Bottom panel */} diff --git a/src/App/ShowAST.tsx b/src/App/ShowAST.tsx index 2480aa2..1e4b586 100644 --- a/src/App/ShowAST.tsx +++ b/src/App/ShowAST.tsx @@ -1,4 +1,4 @@ -import { ConcreteState, PseudoState, stateDescription, Transition } from "../statecharts/abstract_syntax"; +import { ConcreteState, UnstableState, 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 | PseudoState}) { +export const ShowAST = memo(function ShowASTx(props: {root: ConcreteState | UnstableState}) { 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 new file mode 100644 index 0000000..907b531 --- /dev/null +++ b/src/Plant/Microwave/Microwave.css @@ -0,0 +1,14 @@ +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 new file mode 100644 index 0000000..458eb37 --- /dev/null +++ b/src/Plant/Microwave/Microwave.tsx @@ -0,0 +1,183 @@ +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 new file mode 100644 index 0000000..3fe70fa Binary files /dev/null and b/src/Plant/Microwave/bell.wav differ diff --git a/src/Plant/Microwave/running.wav b/src/Plant/Microwave/running.wav new file mode 100644 index 0000000..ca35830 Binary files /dev/null and b/src/Plant/Microwave/running.wav differ diff --git a/src/Plant/Microwave/small_closed_off.png b/src/Plant/Microwave/small_closed_off.png new file mode 100644 index 0000000..3280c99 Binary files /dev/null and b/src/Plant/Microwave/small_closed_off.png differ diff --git a/src/Plant/Microwave/small_closed_on.png b/src/Plant/Microwave/small_closed_on.png new file mode 100644 index 0000000..793166f Binary files /dev/null and b/src/Plant/Microwave/small_closed_on.png differ diff --git a/src/Plant/Microwave/small_opened_off.png b/src/Plant/Microwave/small_opened_off.png new file mode 100644 index 0000000..7c829f0 Binary files /dev/null and b/src/Plant/Microwave/small_opened_off.png differ diff --git a/src/Plant/Microwave/small_opened_on.png b/src/Plant/Microwave/small_opened_on.png new file mode 100644 index 0000000..6f8708a Binary files /dev/null and b/src/Plant/Microwave/small_opened_on.png differ diff --git a/src/VisualEditor/VisualEditor.tsx b/src/VisualEditor/VisualEditor.tsx index 654a0f8..b650c58 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]); + }, [refSVG.current, zoom]); 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 2ed2531..777e680 100644 --- a/src/statecharts/abstract_syntax.ts +++ b/src/statecharts/abstract_syntax.ts @@ -1,20 +1,24 @@ import { Action, EventTrigger, ParsedText } from "./label_ast"; export type AbstractState = { + kind: string; uid: string; parent?: ConcreteState; - comments: [string, string][]; // array of tuple (text-uid, text-text) - entryActions: Action[]; - exitActions: Action[]; depth: number; + comments: [string, string][]; // array of tuple (text-uid, text-text) } -export type StableState = { +export type EntryExitState = AbstractState & { + entryActions: Action[]; + exitActions: Action[]; +} + +export type StableState = EntryExitState & { 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"; @@ -27,25 +31,24 @@ export type OrState = { initial: [string, ConcreteState][]; } & StableState; -export type PseudoState = { - kind: "pseudo"; - uid: string; - comments: [string, string][]; -}; +export type ConcreteState = AndState | OrState; -export type HistoryState = { +export type TransitionSrcTgt = ConcreteState | UnstableState; + +// also called pseudo-state or choice-state: +export type UnstableState = EntryExitState & { + kind: "pseudo"; +} & AbstractState; + +export type HistoryState = AbstractState & { 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 | PseudoState; - tgt: ConcreteState | PseudoState | HistoryState; + src: ConcreteState | UnstableState; + tgt: ConcreteState | UnstableState | HistoryState; label: ParsedText[]; } @@ -59,7 +62,7 @@ export type Statechart = { internalEvents: EventTrigger[]; outputEvents: Set; - uid2State: Map; + uid2State: Map; historyStates: HistoryState[]; } @@ -110,7 +113,7 @@ export function isOverlapping(a: ConcreteState, b: ConcreteState): boolean { } -export function computeLCA(a: (ConcreteState|HistoryState), b: (ConcreteState|HistoryState)): (ConcreteState|HistoryState) { +export function computeLCA(a: AbstractState, b: AbstractState): AbstractState { if (a === b) { return a; } @@ -120,77 +123,90 @@ export function computeLCA(a: (ConcreteState|HistoryState), b: (ConcreteState|Hi return computeLCA(a, b.parent!); } -export function computeLCA2(states: (ConcreteState|HistoryState)[]): (ConcreteState|HistoryState) { - if (states.length === 0) { - throw new Error("cannot compute LCA of empty set of states"); +// 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!; } - if (states.length === 1) { - return states[0]; - } - // 2 states or more - return states.reduce((acc, cur) => computeLCA(acc, cur)); + return arena as OrState; } -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 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 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 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; +// } // 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: ConcreteState, descendant: (ConcreteState|HistoryState)}): (ConcreteState|HistoryState)[] { +export function computePath({ancestor, descendant}: {ancestor: AbstractState, descendant: AbstractState}): AbstractState[] { 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]); - for (const child of state.children) { - for (const descendant of getDescendants(child)) { - // will include child itself: - result.add(descendant); + if (state.children) { + for (const child of state.children) { + for (const descendant of getDescendants(child)) { + // will include child itself: + result.add(descendant); + } } } return result; @@ -199,17 +215,18 @@ 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: ConcreteState | PseudoState | HistoryState): string { +export function stateDescription(state: AbstractState): 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)})`; + return `deep(${stateDescription(state.parent!)})`; + } + else if (state.comments.length > 0) { + return state.comments[0][1]; } else { - // @ts-ignore - const description = state.comments.length > 0 ? state.comments[0][1] : state.uid; - return description; + return state.uid; } } diff --git a/src/statecharts/environment.ts b/src/statecharts/environment.ts new file mode 100644 index 0000000..d53dfa2 --- /dev/null +++ b/src/statecharts/environment.ts @@ -0,0 +1,102 @@ +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 684d81e..c19faa0 100644 --- a/src/statecharts/interpreter.ts +++ b/src/statecharts/interpreter.ts @@ -1,16 +1,21 @@ -import { computeArena2, computePath, ConcreteState, getDescendants, HistoryState, isOverlapping, OrState, StableState, Statechart, stateDescription, Transition, transitionDescription } from "./abstract_syntax"; +import { AbstractState, computeArena, computePath, ConcreteState, getDescendants, HistoryState, isOverlapping, OrState, StableState, Statechart, stateDescription, Transition, transitionDescription, TransitionSrcTgt } from "./abstract_syntax"; import { evalExpr } from "./actionlang_interpreter"; +import { Environment, FlatEnvironment, ScopedEnvironment } from "./environment"; import { Action, EventTrigger, TransitionLabel } from "./label_ast"; -import { BigStepOutput, Environment, initialRaised, Mode, RaisedEvents, RT_Event, RT_History, RT_Statechart, TimerElapseEvent, Timers } from "./runtime_types"; +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); export function initialize(ast: Statechart): BigStepOutput { let history = new Map(); let enteredStates, environment, rest; ({enteredStates, environment, history, ...rest} = enterDefault(0, ast.root, { - environment: new Environment([new Map([ - ["_timers", []], - ["_log", (str: string) => console.log(str)], - ])]), + environment: initialScopedEnvironment, history, ...initialRaised, })); @@ -66,42 +71,49 @@ export function execAction(action: Action, rt: ActionScope): ActionScope { throw new Error("should never reach here"); } -export function entryActions(simtime: number, state: ConcreteState, actionScope: ActionScope): ActionScope { - // console.log('enter', stateDescription(state), '...'); +export function entryActions(simtime: number, state: TransitionSrcTgt, actionScope: ActionScope): ActionScope { + console.log('enter', stateDescription(state), '...'); + let {environment, ...rest} = actionScope; - // environment = environment.pushScope(); + + environment = environment.enterScope(state.uid); + for (const action of state.entryActions) { ({environment, ...rest} = execAction(action, {environment, ...rest})); } // schedule timers - // we store timers in the environment (dirty!) - environment = environment.transform("_timers", oldTimers => { + if (state.kind !== "pseudo") { + // we store timers in the environment (dirty!) + const timers: Timers = environment.get("_timers") || []; const newTimers = [ - ...oldTimers, + ...timers, ...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]); - return newTimers; - }, []); - // new nested scope + newTimers.sort((a,b) => a[0] - b[0]); // earliest timers come first + environment = environment.set("_timers", newTimers); + } return {environment, ...rest}; } -export function exitActions(simtime: number, state: ConcreteState, {enteredStates, ...actionScope}: EnteredScope): ActionScope { - // console.log('exit', stateDescription(state), '...'); +export function exitActions(simtime: number, state: TransitionSrcTgt, {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 - environment = environment.transform("_timers", oldTimers => { - // remove all timers of 'state': - return oldTimers.filter(([_, {state: s}]) => s !== state.uid); - }, []); - // environment = environment.popScope(); + 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(); + return {...actionScope, environment}; } @@ -182,32 +194,37 @@ 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... - for (const child of state.children) { - ({history, ...actionScope} = exitCurrent(simtime, child, {enteredStates, history, ...actionScope})); + if (state.children) { + 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 - 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) - ); + 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) + ); + } } } } @@ -215,82 +232,106 @@ export function exitCurrent(simtime: number, state: ConcreteState, rt: EnteredSc return {history, ...actionScope}; } -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(); +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); for (const state of activeParent.children) { - 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)'); - } + if (config.mode.has(state.uid)) { + const didFire = attemptSrcState(simtime, state, event, statechart, {...config, arenasFired}); + if (didFire) { + ({arenasFired, ...config} = didFire); } else { // no enabled outgoing transitions, try the children: - ({environment, mode, ...rest} = handleEvent(simtime, event, statechart, state, - {environment, mode, ...rest})); + console.log('attempt children'); + ({arenasFired, ...config} = fairStep(simtime, event, statechart, state, {...config, arenasFired})); } } } - return {environment, mode, ...rest}; + return {arenasFired, ...config}; } 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} = handleEvent(simtime, event, statechart, statechart.root, {mode, environment, history, ...raised})); + ({mode, environment, ...raised} = fairStep(simtime, event, statechart, statechart.root, {mode, environment, history, arenasFired: [], ...raised})); return handleInternalEvents(simtime, statechart, {mode, environment, history, ...raised}); } @@ -298,77 +339,127 @@ 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} = handleEvent(simtime, + ({internalEvents, ...rest} = fairStep(simtime, {kind: "input", ...nextEvent}, // internal event becomes input event - statechart, statechart.root, {internalEvents: remainingEvents, ...rest})); + statechart, statechart.root, { arenasFired: [], internalEvents: remainingEvents, ...rest})); } return 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)); +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; + } +} - const srcPath = computePath({ancestor: arena, descendant: t.src as ConcreteState}).reverse() as ConcreteState[]; +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}) 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 the states we need to exit + const exitedMode = mode.difference(toExit); // active states after exiting - // console.log({exitedMode}); + console.log('toExit', toExit); + console.log('exitedMode', 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 { - // exec transition actions + // transition actions for (const action of label.actions) { - ({environment, history, firedTransitions, ...raised} = execAction(action, {environment, history, firedTransitions, ...raised})); + ({environment, history, ...rest} = execAction(action, {environment, history, ...rest})); } - firedTransitions = [...firedTransitions, t.uid]; + 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))); - 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); + let enteredStates; + ({enteredStates, environment, history, ...rest} = enterStates(simtime, state, toEnter, {environment, history, ...rest})); + const enteredMode = exitedMode.union(enteredStates); - // console.log({enteredMode}); + console.log('new mode', enteredMode); - return {mode: enteredMode, environment, history, firedTransitions, ...raised}; - } + console.log('done firing', transitionDescription(t)); + + return {mode: enteredMode, environment, history, ...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)); + +// const srcPath = computePath({ancestor: arena, descendant: t.src as ConcreteState}).reverse() as ConcreteState[]; + +// // 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)); +// } + +// // 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}); + +// return {mode: enteredMode, environment, history, firedTransitions, ...raised}; +// } +// } diff --git a/src/statecharts/mtl/ast.ts b/src/statecharts/mtl/ast.ts new file mode 100644 index 0000000..72d6432 --- /dev/null +++ b/src/statecharts/mtl/ast.ts @@ -0,0 +1,247 @@ +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 new file mode 100644 index 0000000..5ae2e79 --- /dev/null +++ b/src/statecharts/mtl/evaluator.ts @@ -0,0 +1,50 @@ +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 new file mode 100644 index 0000000..924528a --- /dev/null +++ b/src/statecharts/mtl/helpers.ts @@ -0,0 +1,9 @@ + +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 new file mode 100644 index 0000000..7b58f6c --- /dev/null +++ b/src/statecharts/mtl/signals.ts @@ -0,0 +1,149 @@ +// 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 d53388a..a7d1862 100644 --- a/src/statecharts/parser.ts +++ b/src/statecharts/parser.ts @@ -1,4 +1,4 @@ -import { ConcreteState, HistoryState, OrState, PseudoState, Statechart, stateDescription, Transition } from "./abstract_syntax"; +import { ConcreteState, HistoryState, OrState, UnstableState, 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,11 +116,18 @@ export function parseStatechart(state: VisualEditorState, conns: Connections): [ uid2State.set(rt.uid, state as ConcreteState); } for (const d of state.diamonds) { - uid2State.set(d.uid, { + const parent = findParent(d); + const pseudoState = { 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 ec99da9..3d65d4a 100644 --- a/src/statecharts/runtime_types.ts +++ b/src/statecharts/runtime_types.ts @@ -1,3 +1,5 @@ +import { Environment } from "./environment"; + export type Timestamp = number; // milliseconds since begin of simulation export type RT_Event = InputEvent | TimerElapseEvent; @@ -17,80 +19,6 @@ 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 new file mode 100644 index 0000000..3a06076 --- /dev/null +++ b/src/statecharts/scope_tree.ts @@ -0,0 +1,88 @@ +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 73444e0..a82e787 100644 --- a/todo.txt +++ b/todo.txt @@ -27,6 +27,9 @@ TODO +- bugs + interpreter: pseudo-state semantics is broken + - testing use STL for testing https://github.com/mvcisback/py-metric-temporal-logic @@ -36,11 +39,18 @@ 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