Skip to content

Feat/cdd deferred compute #103

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

Open
Brandhoej wants to merge 16 commits into
base: main
Choose a base branch
from
Open

Feat/cdd deferred compute #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
7e425d9
feat(DeferredProeprty): Added a deferred property and tests
Mar 30, 2023
ce8303b
feat(CDD): Made CDD partially use Deferred properties
Mar 30, 2023
175152a
doc(CDD): Added documentation to all deferred proeprties used in CDD
Mar 30, 2023
395f25b
fix(CDD): Made terminal isTrue and equivTrue clear
Mar 30, 2023
cd8d94a
fix(CDD): Removed Log calls
Mar 30, 2023
3b1a581
fix(CDD): Reintroduced the minus commented optimisations
Mar 30, 2023
ea7f3b3
typo(DeferredProperty): Suggestions from W103
Apr 13, 2023
375ade2
fix(DeferredProperty): Descirptions and get/getValue names
Apr 13, 2023
a010948
fix(DeferredProeprtyTest): Adde ending newline
Apr 13, 2023
7b153ad
type(CDD): Added suggestions from #103
Apr 13, 2023
42c9819
fix(CDD): Removed TODO
Apr 13, 2023
1907f58
Merge branch 'feat/CDD-deferred-compute' of https://github.com/Brandh…
Apr 13, 2023
8fcd3df
refactor(Pruning): Removed double negation on false equiv check
Apr 13, 2023
f83f1c8
fix(DeferredProperty): Removed large if statement
Apr 13, 2023
15988ba
fix(CDD): Descriptions and typos
Apr 13, 2023
8376162
fix(tests): Ignores two tests that probably consistenly fails because…
Apr 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/logic/Pruning.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,7 +294,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
// apply updates as guard
//incCDD = CDD.applyReset(incCDD,e.getUpdates());

if (incCDD.isFalse()) {
if (incCDD.equivFalse()) {
// Checking for satisfiability after clocks were reset (only a problem because target invariant might now be x>4)
// if unsatisfiable => keep edge // todo: is return the right thing here?
if (printComments)
Expand All @@ -310,7 +310,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map


// if the inconsistent part cannot be reached, we can ignore the edge e, and go on
if (incCDD.isFalse()) {
if (incCDD.equivFalse()) {
if (printComments)
Log.debug("could not reach inconsistent part, fed is empty");
} else {
Expand Down Expand Up @@ -364,7 +364,7 @@ public CDD backExplorationOnTransition(Edge e, CDD incCDD)
if (printComments)
Log.debug("Invariants done");

if (incCDD.isNotFalse()) {
if (incCDD.notEquivFalse()) {
if (printComments)
Log.debug("Inconsistent part is reachable with this transition. ");
} else {
Expand Down Expand Up @@ -403,7 +403,7 @@ public static void removeTransitionIfUnsat(Edge e, CDD incCDD, List<Edge> edges
testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getSource().getInconsistentPart());


if (!testForSatEdgeCDD.isNotFalse()) {
if (testForSatEdgeCDD.equivFalse()) {
edges.remove(e);
}
if (printComments)
Expand All @@ -416,7 +416,7 @@ public static void processSourceLocation(Edge e, CDD incCDD, Map<Location, CDD>
// If that federation is unsatisfiable, we can just ignore the transition to inc, and be done,
// so we check for that, zone by zone. Only one zone needs to be sat.

if (incCDD.isFalse())
if (incCDD.equivFalse())
{
if (printComments)
Log.debug("Did not add a new inconsistent part");
Expand Down Expand Up @@ -468,7 +468,7 @@ public static CDD predtOfAllOutputs(Edge e, CDD incCDD, List<Edge> edges)

// constrain it by the guards and invariants of the "good transition". TODO: IMPORTANT: Check if the order of doing the target invariant first, freeing, etc. is the correct one

if (goodCDD.isNotFalse()) {
if (goodCDD.notEquivFalse()) {
goodCDD = goodCDD.transitionBack(otherEdge);
//goodCDD = CDD.applyReset(goodCDD, otherEdge.getUpdates());

Expand Down
11 changes: 5 additions & 6 deletions src/logic/Refinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package logic;

import lib.CDDLib;
import log.Log;
import models.*;

Expand Down Expand Up @@ -266,7 +265,7 @@ private StatePair buildStatePair(Transition leaderTransition, Transition followe

// check if there is a part of the CDD where both leader and follower are enabled, abort otherwise
leaderTarget.applyGuards(followerTransition.getGuardCDD());
if (leaderTarget.getInvariant().isFalse()) {
if (leaderTarget.getInvariant().equivFalse()) {
return null;
}

Expand All @@ -275,11 +274,11 @@ private StatePair buildStatePair(Transition leaderTransition, Transition followe

// check target invariants to see if transitions are actually enabled
CDD leaderTargetInvariant = leaderTransition.getTarget().getLocationInvariant();
if (leaderTarget.getInvariant().conjunction(leaderTargetInvariant).isFalse())
if (leaderTarget.getInvariant().conjunction(leaderTargetInvariant).equivFalse())
return null;

CDD followerTargetInvariant = followerTransition.getTarget().getLocationInvariant();
if (leaderTarget.getInvariant().conjunction(followerTargetInvariant).isFalse())
if (leaderTarget.getInvariant().conjunction(followerTargetInvariant).equivFalse())
return null;

// forward explored both transitions, reaching the new target states
Expand Down Expand Up @@ -317,7 +316,7 @@ private boolean createNewStatePairs(List<Transition> trans1, List<Transition> tr
rightCDD = rightCDD.disjunction(c);

// If trans2 does not satisfy all solution of trans1, return empty list which should result in refinement failure
if (!isInput && leftCDD.minus(rightCDD).isNotFalse()) {
if (!isInput && leftCDD.minus(rightCDD).notEquivFalse()) {
Log.info("trans 2 does not satisfiy all solutions of trans 1");
Log.debug("trans 2 does not satisfiy all solutions " + trans2.get(0).getEdges().get(0).getChan());
Log.debug(leftCDD);
Expand All @@ -326,7 +325,7 @@ private boolean createNewStatePairs(List<Transition> trans1, List<Transition> tr
return false;
}

if (isInput && rightCDD.minus(leftCDD).isNotFalse()) {
if (isInput && rightCDD.minus(leftCDD).notEquivFalse()) {
Log.info("trans 2 does not satisfiy all solutions of trans 1");
// Log.debug("trans 2 does not satisfiy all solutions " + trans2.get(0).getEdges().get(0).getChan());
Log.debug(leftCDD);
Expand Down
2 changes: 1 addition & 1 deletion src/logic/SimpleTransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ public boolean checkMovesOverlap(List<Transition> trans) {



if (state1.getInvariant().isNotFalse() && state2.getInvariant().isNotFalse()) {
if (state1.getInvariant().notEquivFalse() && state2.getInvariant().notEquivFalse()) {
if(state1.getInvariant().intersects(state2.getInvariant())) {
Log.debug(trans.get(i).getGuardCDD().getGuard(clocks.getItems()));
Log.debug(trans.get(j).getGuardCDD().getGuard(clocks.getItems()));
Expand Down
4 changes: 2 additions & 2 deletions src/logic/State.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ public void applyResets(List<Update> resets) {
}

public void extrapolateMaxBounds(HashMap<Clock,Integer> maxBounds, List<Clock> relevantClocks){
if (invarCDD.isTrue())
if (invarCDD.equivTrue())
return;
CDD bcddLeftToAnalyse = new CDD(invarCDD.getPointer());
CDD resCDD = CDD.cddFalse();
Expand Down Expand Up @@ -113,7 +113,7 @@ public void extrapolateMaxBounds(HashMap<Clock,Integer> maxBounds, List<Clock> r
}

public void extrapolateMaxBoundsDiag(HashMap<Clock,Integer> maxBounds, List<Clock> relevantClocks){
if (invarCDD.isTrue())
if (invarCDD.equivTrue())
return;
CDD copy = new CDD(invarCDD.getPointer());
CDD resCDD = CDD.cddFalse();
Expand Down
4 changes: 2 additions & 2 deletions src/logic/TransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ private Transition createNewTransition(State state, Move move) {
* that the edge guard is false and thereby the conjunction
* (Applying the edge guard) will result in a contradiction. */
CDD guardCDD = CDD.cddFalse();
if (!edgeGuard.isFalse()) {
if (!edgeGuard.equivFalse()) {
guardCDD = state.getInvariant().conjunction(edgeGuard);
}

Expand Down Expand Up @@ -118,7 +118,7 @@ public List<Transition> createNewTransitions(State state, List<Move> moves, List
Transition transition = createNewTransition(state, move);

// Check if it is unreachable and if so then ignore it
if (transition.getTarget().getInvariant().isFalse()) {
if (transition.getTarget().getInvariant().equivFalse()) {
continue;
}

Expand Down
6 changes: 3 additions & 3 deletions src/models/Automaton.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,17 +286,17 @@ public void makeInputEnabled() {
}

// If the enabled part is true then the disabled part will be false.
if (enabledPart.isTrue()) {
if (enabledPart.equivTrue()) {
continue;
}

// If there is any solution to the enabled CDD then subtract it from the invariant.
if (enabledPart.isNotFalse()) {
if (enabledPart.notEquivFalse()) {
disabledPart = disabledPart.minus(enabledPart);
}

// If there is any solution to the disabled CDD then create an edge.
if (disabledPart.isNotFalse()) {
if (disabledPart.notEquivFalse()) {
Edge newEdge = new Edge(location, location, input, true, disabledPart.getGuard(), new ArrayList<>());
getEdges().add(newEdge);
}
Expand Down
Loading