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.

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

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

Conversation

lemmy
Copy link
Member

@lemmy lemmy commented Apr 6, 2024

Opening a PR, even though this is likely lacking in documentation and too technical to serve as a good example. On the other hand, the more, the merrier. :-)

`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]>
shutdown/terminate nodes after termination *detection* by high-level
specs.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
shutdown functionality.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
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]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>
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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging this pull request may close these issues.

1 participant