Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Composition of specifications #132

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Composition of specifications #132

wants to merge 8 commits into from

Commits on Apr 6, 2024

  1. Add definition of OpenSpec that allows the variables inbox and 

    `count` to change independently of its next-state relation `Next`.  In
other words, we expect `inbox` and `count` to be shared variables with
another component/spec.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    08d8028 View commit details
    Browse the repository at this point in the history

  2. Experiment with *extending* EWD998ChanID to add functionality to 

    shutdown/terminate nodes after termination *detection* by high-level
specs.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    09aedf7 View commit details
    Browse the repository at this point in the history

  3. *Refine* (not extend as in previous commit) the spec EWD998ChanID to add 

    shutdown functionality.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    527d34c View commit details
    Browse the repository at this point in the history

  4. Basic concept how two component specification can combined. 

    Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    6ffadc8 View commit details
    Browse the repository at this point in the history

  5. If spec A has more than a one variable that does not appear in the other 

    spec, we unfortunately have to adapt the composition and create more
restsOfTheUniverse.

The next-state relation of this composition evaluates to false after the
initial state, because it defines variables z and zz to always have
equal values.  This is only satisfied in the special case where the
values of variables z and zz in A are equal throughout all behaviors
(e.g. Init changed to ... /\ zz = TRUE).

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    72d67ae View commit details
    Browse the repository at this point in the history

  6. Nothing to see/Removal of variable zz. 

    Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    666bd56 View commit details
    Browse the repository at this point in the history

  7. If the composition of A and B is such that the every composite behavior 

    is the concatenation of a behavior defined by A and a behavior defined
by B, we won't need the variable `y`.  Instead, Spec is changed to use
ITE with ENABLED evaluated on the next-state relation of spec A.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    e794bb8 View commit details
    Browse the repository at this point in the history

  8. Compose Compute, Detect Termination (EWD998), and Shutdown. 

    Signed-off-by: Markus Alexander Kuppe <[email protected]>
    @lemmy
    lemmy committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    fc16cdc View commit details
    Browse the repository at this point in the history