fix broken pseudo-states (they work more like regular transitions now)
This commit is contained in:
parent
3e192f8e26
commit
43e3b2117c
15 changed files with 1038 additions and 346 deletions
1
global.d.ts
vendored
1
global.d.ts
vendored
|
|
@ -2,3 +2,4 @@
|
|||
declare module '*.css';
|
||||
declare module '*.png';
|
||||
declare module '*.ttf';
|
||||
declare module '*.wav';
|
||||
|
|
@ -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<any>][] = [
|
||||
["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,33 +369,28 @@ export function App() {
|
|||
</div>
|
||||
</div>}
|
||||
|
||||
{/* top-to-bottom: everything -> bottom panel */}
|
||||
<div className="stackVertical" style={{height:'100%'}}>
|
||||
|
||||
{/* left-to-right: main -> sidebar */}
|
||||
<div className="stackHorizontal" style={{flexGrow:1, overflow: "auto"}}>
|
||||
|
||||
{/* Left: top bar and main editor */}
|
||||
<div style={{flexGrow:1, overflow: "auto"}}>
|
||||
<div style={{height:'100%'}}>
|
||||
{/* top-to-bottom: top bar, editor */}
|
||||
<div className="stackVertical" style={{flexGrow:1, overflow: "auto"}}>
|
||||
{/* Top bar */}
|
||||
<div
|
||||
className="shadowBelow"
|
||||
style={{
|
||||
display: "flex",
|
||||
borderBottom: 1,
|
||||
borderColor: "divider",
|
||||
alignItems: 'center',
|
||||
flex: '0 0 content',
|
||||
}}
|
||||
style={{flex: '0 0 content'}}
|
||||
>
|
||||
{editHistory && <TopPanel
|
||||
{...{trace, time, setTime, onUndo, onRedo, onInit, onClear, onBack, insertMode, setInsertMode, setModal, zoom, setZoom, showKeys, setShowKeys, editHistory}}
|
||||
/>}
|
||||
</div>
|
||||
{/* Below the top bar: Editor */}
|
||||
{/* Editor */}
|
||||
<div style={{flexGrow: 1, overflow: "auto"}}>
|
||||
{editorState && conns && syntaxErrors && <VisualEditor {...{state: editorState, setState: setEditorState, conns, trace, setTrace, syntaxErrors, insertMode, highlightActive, highlightTransitions, setModal, makeCheckPoint, zoom}}/>}
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
{/* Right: sidebar */}
|
||||
<div style={{
|
||||
|
|
@ -406,7 +399,7 @@ export function App() {
|
|||
flex: '0 0 content',
|
||||
overflowY: "auto",
|
||||
overflowX: "visible",
|
||||
maxWidth: 'min(300px, 30vw)',
|
||||
maxWidth: '50vw',
|
||||
}}>
|
||||
<div className="stackVertical" style={{height:'100%'}}>
|
||||
<div
|
||||
|
|
@ -445,7 +438,9 @@ export function App() {
|
|||
)}
|
||||
</select>
|
||||
{trace !== null &&
|
||||
plant.render(trace.trace[trace.idx].plantState, event => onRaise(event.name, event.param))}
|
||||
<div>{
|
||||
plant.render(trace.trace[trace.idx].plantState, event => onRaise(event.name, event.param))
|
||||
}</div>}
|
||||
</PersistentDetails>
|
||||
<details open={showExecutionTrace} onToggle={e => setShowExecutionTrace(e.newState === "open")}><summary>execution trace</summary></details>
|
||||
</div>
|
||||
|
|
@ -467,8 +462,6 @@ export function App() {
|
|||
</div>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
{/* Bottom panel */}
|
||||
|
|
|
|||
|
|
@ -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) || [];
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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<string>;
|
||||
|
||||
uid2State: Map<string, ConcreteState|PseudoState>;
|
||||
uid2State: Map<string, ConcreteState|UnstableState>;
|
||||
|
||||
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,96 +123,110 @@ 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<string, Transition[]>): (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<string, Transition[]>): 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<string, Transition[]>): (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<string, Transition[]>): 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<string> {
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
// 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;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
102
src/statecharts/environment.ts
Normal file
102
src/statecharts/environment.ts
Normal file
|
|
@ -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<string, any>;
|
||||
|
||||
constructor(env: ReadonlyMap<string, any> = 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);
|
||||
}
|
||||
}
|
||||
|
|
@ -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<string, any>([
|
||||
["_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<string, any>([
|
||||
["_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
|
||||
if (state.kind !== "pseudo") {
|
||||
// we store timers in the environment (dirty!)
|
||||
environment = environment.transform<Timers>("_timers", oldTimers => {
|
||||
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>("_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,18 +194,22 @@ 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}));
|
||||
}
|
||||
}
|
||||
|
||||
// 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") {
|
||||
|
|
@ -211,20 +227,28 @@ 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<OrState>();
|
||||
for (const state of activeParent.children) {
|
||||
if (mode.has(state.uid)) {
|
||||
const outgoing = statechart.transitions.get(state.uid) || [];
|
||||
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]) =>
|
||||
|
|
@ -235,62 +259,79 @@ export function handleEvent(simtime: number, event: RT_Event, statechart: Statec
|
|||
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 guardEnvironment = environment.set("inState", (stateLabel: string) => {
|
||||
const 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));
|
||||
};
|
||||
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(state)}' has multiple (${enabled.length}) enabled outgoing transitions: ${enabled.map(([t]) => transitionDescription(t)).join(', ')}`, [...enabled.map(([t]) => t.uid), state.uid]);
|
||||
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 [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;
|
||||
const [toFire, label] = enabled[0];
|
||||
const arena = computeArena(toFire.src, toFire.tgt);
|
||||
if (allowedToFire(arena, arenasFired)) {
|
||||
environment = environment.enterScope("<transition>");
|
||||
// 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};
|
||||
}
|
||||
}
|
||||
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,
|
||||
);
|
||||
return {mode, environment, arenasFired, ...rest};
|
||||
}
|
||||
({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)');
|
||||
}
|
||||
|
||||
// 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 (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<string, Transition[]>, 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<string> {
|
||||
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<string, Transition[]>, 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<string, Transition[]>, 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];
|
||||
|
||||
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<string>;
|
||||
}
|
||||
else {
|
||||
toEnter = new Set(tgtPath.map(s=>s.uid));
|
||||
}
|
||||
const state = tgtPath[0] as ConcreteState; // first state to enter
|
||||
const toEnter = resolveHistory(t.tgt, history)
|
||||
.union(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);
|
||||
({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<string, Transition[]>, 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<string, Transition[]>, 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<string>;
|
||||
// }
|
||||
// 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};
|
||||
// }
|
||||
// }
|
||||
|
|
|
|||
247
src/statecharts/mtl/ast.ts
Normal file
247
src/statecharts/mtl/ast.ts
Normal file
|
|
@ -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<t; i++) {
|
||||
expr = new Next(expr);
|
||||
}
|
||||
return expr;
|
||||
}
|
||||
|
||||
function* _walk(expr) {
|
||||
const children = [expr];
|
||||
while (children.length > 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);
|
||||
50
src/statecharts/mtl/evaluator.ts
Normal file
50
src/statecharts/mtl/evaluator.ts
Normal file
|
|
@ -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
|
||||
}
|
||||
9
src/statecharts/mtl/helpers.ts
Normal file
9
src/statecharts/mtl/helpers.ts
Normal file
|
|
@ -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,
|
||||
});
|
||||
}
|
||||
149
src/statecharts/mtl/signals.ts
Normal file
149
src/statecharts/mtl/signals.ts
Normal file
|
|
@ -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<Time, Map<KeyType, ValueType>>;
|
||||
|
||||
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<KeyType,ValueType>) => Map<KeyType,ValueType>) {
|
||||
const data = new Map([
|
||||
...this.data.entries().map(([key, val]) =>
|
||||
[key, f(val)] as [Time, any])]);
|
||||
return _evolve(this, {
|
||||
data,
|
||||
});
|
||||
}
|
||||
|
||||
map(f: (val: Map<KeyType,ValueType>) => Map<KeyType,ValueType>, 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<KeyType,ValueType>) => boolean) {
|
||||
return _evolve(this, {
|
||||
data: new Map([...this.data.entries().filter(([_, val]) => f(val))]),
|
||||
});
|
||||
}
|
||||
|
||||
project(keys: Set<KeyType>) {
|
||||
return this
|
||||
.transform(val => new Map([...val.entries()].filter(([key]) => keys.has(key))))
|
||||
.filter(val => keys.intersection(val.keys()).size > 0);
|
||||
}
|
||||
|
||||
retag(mapping: Map<KeyType, KeyType>) {
|
||||
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);
|
||||
}
|
||||
|
|
@ -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<string, ConcreteState|PseudoState>([["root", root]]);
|
||||
const uid2State = new Map<string, ConcreteState|UnstableState>([["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}});
|
||||
|
|
|
|||
|
|
@ -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<string>; // set of active states
|
||||
|
||||
export class Environment {
|
||||
scopes: ReadonlyMap<string, any>[]; // array of nested scopes - scope at the back of the array is used first
|
||||
|
||||
constructor(env = [new Map()] as ReadonlyMap<string, any>[]) {
|
||||
this.scopes = env;
|
||||
}
|
||||
|
||||
pushScope(): Environment {
|
||||
return new Environment([...this.scopes, new Map<string, any>()]);
|
||||
}
|
||||
|
||||
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<T>(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<string, Set<string>>;
|
||||
|
||||
export type RT_Statechart = {
|
||||
|
|
|
|||
88
src/statecharts/scope_tree.ts
Normal file
88
src/statecharts/scope_tree.ts
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
export type ScopeTree = {
|
||||
env: ReadonlyMap<string, any>;
|
||||
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];
|
||||
}
|
||||
}
|
||||
}
|
||||
12
todo.txt
12
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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue