behavior.sysml

// How the pipeline behaves: one analysis run, the tier gating that decides how
// far it gets, the two execution engines the runtime drives, and the analysis
// framework that turns a question into a plan.
package OpenSysMLBehavior {
    private import ScalarValues::*;
    private import OpenSysMLArtifacts::*;

    attribute def EditEvent;
    attribute def TokenArrival;
    attribute def SignalEvent;

    // One document analysed end to end. The tiers decide whether lowering and
    // execution are reached at all.
    action def AnalyzeDocument {
        attribute syntaxErrors : Integer = 0;
        attribute semanticErrors : Integer = 0;
        attribute executable : Boolean = true;

        in item text : SourceText;
        out item findings : Diagnostic;
        out item trace : ExecutionTrace;

        first start;

        action scan;
        action parse;
        action buildScopes;
        action resolveNames;
        action buildSemanticModel;

        action runSyntaxTier;
        action runNameTier;
        action runTypeTier;
        action runConstraintTier;

        action lower;
        action execute;
        action publish;

        succession first start then scan;
        succession first scan then parse;
        succession first parse then buildScopes;
        succession first buildScopes then resolveNames;
        succession first resolveNames then buildSemanticModel;
        succession first buildSemanticModel then runSyntaxTier;
        succession first runSyntaxTier then syntaxGate;

        // A failed tier stops the tiers above it; diagnostics are still published.
        decide syntaxGate;
        if syntaxErrors == 0 then runNameTier;
        else publish;

        succession first runNameTier then nameGate;

        decide nameGate;
        if semanticErrors == 0 then runTypeTier;
        else publish;

        succession first runTypeTier then typeGate;

        decide typeGate;
        if semanticErrors == 0 then runConstraintTier;
        else publish;

        succession first runConstraintTier then executionGate;

        decide executionGate;
        if executable then lower;
        else publish;

        succession first lower then execute;
        succession first execute then publish;
        succession first publish then done;
    }

    // The editor path: an edit reanalyses its own document immediately and
    // sweeps the other open ones once the burst settles.
    action def ServeEdit {
        in item edit : SourceText;
        out item findings : Diagnostic;

        first start;

        action applyEdit;
        action reanalyzeEdited;
        action publishEdited;
        action debounce;
        action sweepOpenDocuments;

        succession first start then applyEdit;
        succession first applyEdit then reanalyzeEdited;
        succession first reanalyzeEdited then split;

        fork split;
        succession first split then publishEdited;
        succession first split then debounce;
        succession first debounce then sweepOpenDocuments;
        succession first publishEdited then sync;
        succession first sweepOpenDocuments then sync;

        join sync;
        succession first sync then done;
    }

    // The library loaded once per process: the snapshot when it was written from
    // these files and decodes intact, the files otherwise.
    action def LoadLibrary {
        attribute snapshotCurrent : Boolean = true;
        attribute snapshotIntact : Boolean = true;

        in item snapshotBlob : LibrarySnapshot;
        out item index : SymbolIndex;

        first start;

        action digestFiles;
        action readHeader;
        action verifyChecksum;
        action decodeSnapshot;
        action parseFiles;
        action indexFiles;
        action expandImports;
        action freeze;
        action share;

        succession first start then digestFiles;
        succession first digestFiles then readHeader;
        succession first readHeader then digestGate;

        // A snapshot of other files, another format or an override parses.
        decide digestGate;
        if snapshotCurrent then verifyChecksum;
        else parseFiles;

        succession first verifyChecksum then checksumGate;

        decide checksumGate;
        if snapshotIntact then decodeSnapshot;
        else parseFiles;

        succession first parseFiles then indexFiles;
        succession first indexFiles then expandImports;
        succession first expandImports then freeze;
        succession first decodeSnapshot then share;
        succession first freeze then share;
        succession first share then done;
    }

    // The tier ladder as states: each tier is entered only from a clean tier
    // below it, and any failure halts short of execution.
    state def TierProgression {
        attribute failures : Integer = 0;
        attribute elementScopedPending : Boolean = false;

        entry; then syntaxTier;

        state syntaxTier;
        state nameTier;
        state typeTier;
        state constraintTier {
            entry; then documentScoped;

            state documentScoped;
            state elementScoped;

            // An element-scoped pass still runs for subjects that are not
            // downstream of the failure.
            transition documentScoped_to_elementScoped
                first documentScoped
                if elementScopedPending
                then elementScoped;
        }
        state executing;
        state halted;

        transition first syntaxTier if failures == 0 then nameTier;
        transition first syntaxTier if failures > 0 then halted;
        transition first nameTier if failures == 0 then typeTier;
        transition first nameTier if failures > 0 then halted;
        transition first typeTier if failures == 0 then constraintTier;
        transition first typeTier if failures > 0 then halted;
        transition first constraintTier if failures == 0 then executing;
        transition first constraintTier if failures > 0 then halted;
    }

    // One calc invocation: a scalar body — locals, returns, conditionals, library
    // intrinsics, named arguments — runs compiled unless the run is traced or an
    // argument is not a scalar or leaves a parameter unbound; the answer is the same.
    action def InvokeCalc {
        attribute tierEnabled : Boolean = true;
        attribute untraced : Boolean = true;
        attribute bodyIsScalar : Boolean = true;
        attribute scalarArguments : Boolean = true;

        first start;

        action bindArguments;
        action compileBody;
        action runCompiled;
        action boxResult;
        action evaluateBody;

        succession first start then bindArguments;
        succession first bindArguments then traceGate;

        // A traced run records every sub-expression, which only the evaluator does.
        decide traceGate;
        if tierEnabled and untraced then bodyGate;
        else evaluateBody;

        decide bodyGate;
        if bodyIsScalar then compileBody;
        else evaluateBody;

        succession first compileBody then argumentGate;

        decide argumentGate;
        if scalarArguments then runCompiled;
        else evaluateBody;

        succession first runCompiled then boxResult;
        succession first boxResult then done;
        succession first evaluateBody then done;
    }

    // One feature read on one object: the value is made the first time it is asked for,
    // by the case its feature is in, and passes admission before the object holds it.
    action def ReadFeatureValue {
        attribute declared : Boolean = true;
        attribute materialized : Boolean = false;
        attribute bound : Boolean = false;
        attribute variationFeature : Boolean = false;
        attribute statesValue : Boolean = false;
        attribute fallbackDefault : Boolean = false;
        attribute contributed : Boolean = false;
        attribute connector : Boolean = false;
        attribute composite : Boolean = false;
        attribute abstractFeature : Boolean = false;
        attribute optional : Boolean = false;

        attribute evaluations : Integer = 0;
        attribute objectsMade : Integer = 0;
        attribute admitted : Boolean = false;
        attribute tracked : Boolean = false;
        attribute refused : Boolean = false;

        first start;

        action refuseUnknown { assign refused := true; }
        action refuseUninitialized { assign refused := true; }
        action returnHeld;
        action holdNothing;
        action readFarEnd { assign evaluations := evaluations + 1; }
        action bindVariant { assign evaluations := evaluations + 1; }
        action holdContributions;
        action deriveValue {
            assign evaluations := evaluations + 1;
            assign tracked := true;
        }
        action holdConnectedEnds;
        action makeObjects { assign objectsMade := objectsMade + 1; }
        action admit { assign admitted := true; }

        succession first start then lookupGate;

        // Naming no feature value of the object is no materialization of one.
        decide lookupGate;
        if declared then bindingGate;
        else refuseUnknown;

        // A value bound or connected is read from its far end whatever the feature states.
        decide bindingGate;
        if bound then readFarEnd;
        else heldGate;

        // Written already, or a constant default folded when the object was made.
        decide heldGate;
        if materialized then returnHeld;
        else variationGate;

        // A variation holds the variant its default selects, and nothing until then.
        decide variationGate;
        if variationFeature then bindVariant;
        else fallbackGate;

        // A `default` applies only where no member subsetting the feature contributes.
        decide fallbackGate;
        if statesValue and fallbackDefault and contributed then holdContributions;
        else valueGate;

        // A default that did not fold is derived against the object, so that it sees the
        // sibling values it reads, and re-derived when one of them is written.
        decide valueGate;
        if statesValue then deriveValue;
        else contributionGate;

        // An abstract feature has no values of its own and an optional one demands none:
        // a connector or composite of either kind holds only what subsets it contributes.
        decide contributionGate;
        if (abstractFeature or optional) and (connector or composite) then holdContributions;
        else connectorGate;

        // A connector holds the features at its ends rather than objects of its own.
        decide connectorGate;
        if connector then holdConnectedEnds;
        else compositeGate;

        // Lazy instantiation: a composite feature holds objects of its own.
        decide compositeGate;
        if composite then makeObjects;
        else valuelessGate;

        // Nothing makes a value for a plain feature: it reads as empty when optional, and
        // as uninitialized when required.
        decide valuelessGate;
        if optional then holdNothing;
        else refuseUninitialized;

        succession first readFarEnd then admit;
        succession first bindVariant then admit;
        succession first deriveValue then admit;
        succession first makeObjects then admit;
        succession first holdContributions then admit;
        succession first admit then done;
        succession first returnHeld then done;
        succession first holdConnectedEnds then done;
        succession first holdNothing then done;
        succession first refuseUnknown then done;
        succession first refuseUninitialized then done;
    }

    // The runtime tiers, from an effective feature list to a simulated model.
    state def RuntimeTiers {
        entry; then featureFlattening;

        state featureFlattening;
        state instanceModel;
        state expressionEvaluation;
        state behavioralModel;
        state behavioralExecution;

        transition first featureFlattening then instanceModel;
        transition first instanceModel then expressionEvaluation;
        transition first expressionEvaluation then behavioralModel;
        transition first behavioralModel then behavioralExecution;
    }

    // Token flow: a step moves every enabled token, and a round with no
    // movement is a deadlock rather than a hang. The budget is the action-step one.
    state def TokenFlow {
        attribute progressed : Boolean = true;
        attribute budgetLeft : Integer = 1000000;

        entry; then idle;

        state idle;
        state stepping;
        state blocked;
        state completed;

        transition first idle accept TokenArrival then stepping;
        transition first stepping if progressed and budgetLeft > 0 then idle;
        transition first stepping if not progressed then blocked;
        transition first stepping if budgetLeft <= 0 then blocked;
        transition first idle if not progressed then completed;
    }

    // Event dispatch: run-to-completion; an event no transition and no parked
    // accept takes is dropped.
    state def EventDispatch {
        attribute handled : Boolean = true;

        entry; then waiting;

        state waiting;
        state dispatching;
        state dropped;
        state settled;

        transition first waiting accept SignalEvent then dispatching;
        transition first dispatching if handled then settled;
        transition first dispatching if not handled then dropped;
        transition first dropped then waiting;
        transition first settled then waiting;
    }

    // Eight budgets, each exhausted on its own: the first to run out ends the run
    // with the error that names it, and the others are not consulted.
    state def BudgetExhaustion {
        attribute stepsLeft : Integer = 10000000;
        attribute actionStepsLeft : Integer = 1000000;
        attribute stateEventsLeft : Integer = 1000000;
        attribute doStepsLeft : Integer = 5000000;
        attribute elementsLeft : Integer = 1000000;
        attribute calcDepthLeft : Integer = 10000;
        attribute sweepRunsLeft : Integer = 1000;
        attribute integerBitsLeft : Integer = 1048576;

        entry; then running;

        state running;
        state stepLimitExceeded;
        state actionStepLimitExceeded;
        state stateEventLimitExceeded;
        state doStepLimitExceeded;
        state elementLimitExceeded;
        state calcRecursionLimitExceeded;
        state sweepRunLimitExceeded;
        state integerSizeLimitExceeded;

        transition first running if stepsLeft <= 0 then stepLimitExceeded;
        transition first running if actionStepsLeft <= 0 then actionStepLimitExceeded;
        transition first running if stateEventsLeft <= 0 then stateEventLimitExceeded;
        transition first running if doStepsLeft <= 0 then doStepLimitExceeded;
        transition first running if elementsLeft <= 0 then elementLimitExceeded;
        transition first running if calcDepthLeft <= 0 then calcRecursionLimitExceeded;
        transition first running if sweepRunsLeft <= 0 then sweepRunLimitExceeded;
        transition first running if integerBitsLeft <= 0 then integerSizeLimitExceeded;
    }

    // What a step costs, for the action-step budget the runtime enforces.
    calc def StepBudget {
        in attribute rounds : Integer;
        in attribute tokensPerRound : Integer;
        return attribute steps : Integer = rounds * tokensPerRound;
    }

    // One question answered: the selection decides which engines are consulted,
    // coverage is asked before any work, and every step lands in the plan.
    action def AnswerQuestion {
        attribute selectsAuto : Boolean = true;
        attribute selectsAll : Boolean = false;
        // The engines declaring the question's kind: one for every kind but outcomes, holds
        // and sensitive in the default registry, whose count per kind Dispatcher.candidatesPerKind states.
        attribute candidates : Integer = 1;
        attribute enginesLeft : Integer = 0;
        attribute steps : Integer = 0;
        // The candidates asked first that do not cover the question; the rest do.
        attribute refusing : Integer = 0;
        attribute concluded : Boolean = true;
        attribute faulted : Boolean = false;

        in item question : AnalysisQuestion;
        out item plan : AnalysisPlan;
        out item result : AnalysisResult;

        first start;

        action rankByAuthority { assign enginesLeft := candidates; }
        action listByName { assign enginesLeft := candidates; }
        action pickNamed { assign enginesLeft := 1; }
        action askCoverage { assign enginesLeft := enginesLeft - 1; }
        action recordRefusal {
            assign steps := steps + 1;
            assign refusing := refusing - 1;
        }
        action runEngine;
        action recordResult { assign steps := steps + 1; }
        action nextEngine;
        action compose;
        action recordFault { assign steps := steps + 1; }

        succession first start then selectionGate;

        // Auto ranks the engines declaring the kind strongest first; all consults
        // each of them in name order; a name consults exactly one.
        decide selectionGate;
        if selectsAuto then rankByAuthority;
        if selectsAll and not selectsAuto then listByName;
        else pickNamed;

        succession first rankByAuthority then askCoverage;
        succession first listByName then askCoverage;
        succession first pickNamed then askCoverage;
        succession first askCoverage then coverageGate;

        decide coverageGate;
        if refusing > 0 then recordRefusal;
        else runEngine;

        succession first runEngine then faultGate;

        decide faultGate;
        if faulted then recordFault;
        else recordResult;

        succession first recordFault then done;
        succession first recordResult then standingGate;
        succession first recordRefusal then refusalGate;

        // A refusal is a step and no answer: the next candidate is asked whatever the
        // selection.
        decide refusalGate;
        if enginesLeft > 0 then askNext;
        else composePlan;

        // Auto stops at the first answer that is a claim and moves on from one that is
        // not; all goes on to every engine and composes at the end; a name is done.
        decide standingGate;
        if enginesLeft > 0 and (selectsAll or (selectsAuto and not concluded)) then askNext;
        else composePlan;

        merge askNext;
        merge composePlan;
        succession first askNext then nextEngine;
        succession first composePlan then compose;
        succession first nextEngine then askCoverage;
        succession first compose then done;
    }

    // One run of the explore engine: a queue of schedule prefixes worked by a fleet of
    // workers, each run on a context of its own, until the queue empties or a budget cuts.
    action def ExploreOutcomes {
        attribute jobs : Integer = 1;
        attribute runsLeft : Integer = 1024;
        attribute depth : Integer = 64;
        attribute queued : Integer = 1;
        // The choice tree: a chain of choices of so many alternatives each, the next
        // below alternative `below` of the one above; choicesAhead are unmet yet.
        attribute choicesAhead : Integer = 0;
        attribute alternatives : Integer = 2;
        attribute below : Integer = 1;
        // The prefix in hand: the choice it ends at (0: the empty prefix) and the
        // alternative it takes there; the run records down to choice `reached`, and
        // `open` while the next choice lies below the alternative its record ends at.
        // `met` counts the choices some run has recorded so far.
        attribute choice : Integer = 0;
        attribute taken : Integer = 0;
        attribute reached : Integer = 0;
        attribute open : Boolean = true;
        attribute met : Integer = 0;
        // The first prefix of the level being worked: the prefixes of so many
        // departures from the first run, worked in order of the choice varied.
        attribute levelChoice : Integer = 0;
        attribute levelTaken : Integer = 0;
        // What the run leaves to explore: the second alternative of each choice it met
        // and the next alternative of the choice its prefix ended at.
        attribute unexplored : Integer = 0;
        attribute runsHit : Boolean = false;
        attribute depthHit : Boolean = false;
        attribute complete : Boolean = true;

        in item question : AnalysisQuestion;
        out item result : AnalysisResult;

        first start;

        action warmWorker;
        action takePrefix {
            assign queued := queued - 1;
            assign reached := choice;
            assign open := choice == 0 or taken == below;
        }
        action freshContext;
        action runLinearization { assign runsLeft := runsLeft - 1; }
        action meetChoice {
            assign reached := reached + 1;
            assign met := met + 1;
            assign unexplored := unexplored + 1;
            assign choicesAhead := choicesAhead - 1;
            assign open := below == 1;
        }
        action passBeyond {
            assign depthHit := true;
            assign choicesAhead := 0;
        }
        action runLeaf;
        action leaveNext { assign unexplored := unexplored + 1; }
        action queueChoices {
            assign queued := queued + unexplored;
            assign unexplored := 0;
        }
        action dropBeyond {
            assign queued := runsLeft;
            assign unexplored := 0;
            assign runsHit := true;
        }
        action stepAcross {
            assign choice := choice + 1;
            assign taken := taken - below + 1;
        }
        action startLevel {
            assign choice := levelChoice;
            assign taken := levelTaken;
        }
        action scanAcross {
            assign choice := choice + 1;
            assign taken := taken - below + 1;
        }
        action stepAlong {
            assign taken := taken + 1;
            assign levelChoice := choice;
            assign levelTaken := taken;
        }
        action stepDown {
            assign choice := choice + 1;
            assign taken := 2;
            assign levelChoice := choice;
            assign levelTaken := 2;
        }
        action sortOutcomes { assign complete := not runsHit and not depthHit; }
        action claimProved;
        action claimObserved;

        succession first start then warmWorker;
        succession first warmWorker then takePrefix;
        succession first takePrefix then freshContext;
        succession first freshContext then runLinearization;
        succession first runLinearization then descend;

        // The run takes the first alternative of every choice it meets on the way down:
        // within the depth bound each leaves its second alternative, beyond it none.
        merge descend;
        succession first descend then choiceGate;

        decide choiceGate;
        if choicesAhead > 0 and open and reached < depth then meetChoice;
        if choicesAhead > 0 and open and reached >= depth then passBeyond;
        else runLeaf;

        succession first meetChoice then descend;
        succession first passBeyond then runMade;
        succession first runLeaf then runMade;

        // The choice the prefix ended at is the run's to advance: it leaves the next
        // alternative while one is untried.
        merge runMade;
        succession first runMade then nextGate;

        decide nextGate;
        if choice > 0 and taken < alternatives then leaveNext;
        else cutGate;

        succession first leaveNext then cutGate;

        // The plan never outgrows the run budget: what a run leaves goes on the queue up to
        // the runs left, the rest is dropped and the runs bound is hit.
        merge cutGate;
        succession first cutGate then capGate;

        decide capGate;
        if queued + unexplored > runsLeft then dropBeyond;
        else queueChoices;

        succession first dropBeyond then queueMade;
        succession first queueChoices then queueMade;

        // The queue starts with the empty prefix and grows by what each run leaves
        // within the budget; exploration ends when it drains.
        merge queueMade;
        succession first queueMade then queueGate;

        decide queueGate;
        if queued == 0 then sortOutcomes;
        else headGate;

        // What a run leaves goes to the back of the queue, every departure from the first
        // run before any second one, earliest choice first: the next prefix is the one
        // across the level, else the first child of the level's first prefix that has one.
        decide headGate;
        if choice + 1 <= met and taken >= below + 1 then stepAcross;
        else startLevel;

        succession first stepAcross then takePrefix;
        succession first startLevel then scan;

        merge scan;
        succession first scan then childGate;

        decide childGate;
        if choice > 0 and taken < alternatives then stepAlong;
        if (choice == 0 or taken == below) and choice + 1 <= met then stepDown;
        if choice + 1 <= met and taken >= below + 1 then scanAcross;
        else sortOutcomes;

        succession first scanAcross then scan;
        succession first stepAlong then takePrefix;
        succession first stepDown then takePrefix;

        succession first sortOutcomes then completionGate;

        // Every prefix visited within the bounds is a proof over every schedule; a
        // bound reached is the concrete runs that were made and no more.
        decide completionGate;
        if complete then claimProved;
        else claimObserved;

        succession first claimProved then done;
        succession first claimObserved then done;
    }

    // The evidence scale as a ladder: a result only ever moves up it, and a
    // universal claim with a bound reached comes back down to bounded.
    state def EvidenceLadder {
        attribute refused : Boolean = false;
        attribute concrete : Boolean = true;
        attribute existential : Boolean = false;
        attribute boundReached : Boolean = false;
        attribute exhaustive : Boolean = false;

        entry; then asked;

        state asked;
        state notCovered;
        state observed;
        state witnessed;
        state bounded;
        state proved;

        transition first asked if refused then notCovered;
        transition first asked if not refused and concrete and not existential then observed;
        transition first asked if not refused and existential then witnessed;
        transition first asked if not refused and not concrete and boundReached then bounded;
        transition first asked if not refused and not concrete and not boundReached and exhaustive then proved;
    }

    // A plan's fleet: a worker is built for a job on first use and kept for every later
    // run under that job; each run gets a fresh context on its worker.
    state def WorkerLifecycle {
        attribute built : Boolean = false;
        attribute runsPending : Integer = 1;

        entry; then idle;

        state idle;
        state warming;
        state ready;
        state running;
        state released;

        transition first idle if not built then warming;
        transition first idle if built then ready;
        transition first warming then ready;
        transition first ready if runsPending > 0 then running;
        transition first running do assign runsPending := runsPending - 1 then ready;
        transition first ready if runsPending <= 0 then released;
    }

    // A snapshot is a mark between steps, a paused body's continuation among what it holds:
    // restore brings the run back to it as often as asked until release; mid-step it is refused.
    state def SnapshotLifecycle {
        attribute betweenSteps : Boolean = true;

        entry; then running;

        state running;
        state marked;
        state refusedMidStep;
        state released;

        transition first running if betweenSteps then marked;
        transition first running if not betweenSteps then refusedMidStep;
        transition first marked then running;
        transition first marked then released;
    }
}