Skip to content

Feat/guard short circuit visitor #108

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

Draft
Brandhoej wants to merge 13 commits into
base: main
Choose a base branch
from
Draft

Feat/guard short circuit visitor #108

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 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
0a8364f
feat(CDD): Added CDDFActory and GuardFactory
Mar 30, 2023
3b1a581
fix(CDD): Reintroduced the minus commented optimisations
Mar 30, 2023
6570717
fix(CDD): Removed toBoolGuards
Mar 30, 2023
e34b549
Merge branch 'feat/CDD-deferred-compute' into feat/cdd-factories
Mar 30, 2023
937f7d3
feat(CDDRuntime): Added the CDDRUntime and changed CDD calls everywhere
Mar 30, 2023
2b91401
fix(CDDRuntime): Added clock check
Mar 30, 2023
790c170
feat(DiagonalConstraintRemover): Guard visitor have been implemented
Mar 30, 2023
1243da1
feat(Guard): Simplifiers for the Guard class
Mar 30, 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
4 changes: 3 additions & 1 deletion src/connection/EcdarService.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import logic.Controller;
import logic.query.Query;
import models.CDD;
import models.CDDRuntime;

import java.util.List;

Expand Down Expand Up @@ -86,7 +87,8 @@ public void sendQuery(QueryProtos.Query request,
private String tryEnsureDone(Throwable e) {
String description = e.getClass().getName() + ": " + e.getMessage();

try {CDD.ensureDone(); }
try {
CDDRuntime.ensureDone(); }
catch (Throwable ee) {
description += "\n" + ee.getClass().getName() + ": " + ee.getMessage();
}
Expand Down
6 changes: 3 additions & 3 deletions src/logic/AggregatedTransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ public Automaton getAutomaton() {
try {
resultant = aggregate(automata);
} finally {
CDD.done();
CDDRuntime.done();
}

return resultant;
Expand Down Expand Up @@ -142,7 +142,7 @@ protected Set<Channel> union(Set<Channel> set1, Set<Channel> set2) {
}

private Automaton aggregate(Automaton[] automata) {
boolean initialisedCdd = CDD.tryInit(getClocks(), BVs.getItems());
boolean initialisedCdd = CDDRuntime.tryInit(getClocks(), BVs.getItems());

String name = getName();

Expand Down Expand Up @@ -217,7 +217,7 @@ locations, getClocks(), getClocks(), getBVs(), getBVs()
Automaton resAut = new Automaton(name, updatedLocations, edgesWithNewClocks, clocks.getItems(), BVs.getItems(), false);

if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}

return resAut;
Expand Down
4 changes: 2 additions & 2 deletions src/logic/Bisimilarity.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ public static Automaton checkBisimilarity(Automaton aut1) {
bisimilarLocs.add(locs); // at the start we "assume all locs are bisimilar"


boolean initialisedCdd = CDD.tryInit(clocks, BVs);
boolean initialisedCdd = CDDRuntime.tryInit(clocks, BVs);
thereWasAChange= true;


Expand Down Expand Up @@ -142,7 +142,7 @@ public static Automaton checkBisimilarity(Automaton aut1) {
}

if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return new Automaton(copy.getName()+"Bisimilar",locs,finalEdges,clocks, copy.getBVs());

Expand Down
60 changes: 38 additions & 22 deletions src/logic/Pruning.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ public static SimpleTransitionSystem adversarialPruning(TransitionSystem ts) {
Set<Location> inconsistentLocations;
Map<Location, CDD> passedInconsistentStates;

boolean initialisedCdd = CDD.tryInit(clocks, BVs);
boolean initialisedCdd = CDDRuntime.tryInit(clocks, BVs);


for (Location l : locations) {
Expand Down Expand Up @@ -86,7 +86,7 @@ public static SimpleTransitionSystem adversarialPruning(TransitionSystem ts) {
}

if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}

Automaton resAut = new Automaton(aut.getName(), locations, edges, clocks, aut.getBVs(), true);
Expand Down Expand Up @@ -142,7 +142,8 @@ public static void addInconsistentPartsToInvariants(List<Location> locations, Li
l.setInvariantGuard(new FalseGuard());
}
else {
CDD invarMinusIncCDD = new CDD(l.getInvariantGuard()).minus(l.getInconsistentPart());
CDD invariantCDD = CDDFactory.createFrom(l.getInvariantGuard());
CDD invarMinusIncCDD = invariantCDD.minus(l.getInconsistentPart());
l.setInvariantGuard(invarMinusIncCDD.getGuard(clocks));
}
}
Expand All @@ -158,9 +159,10 @@ public static void addInvariantsToGuards(List<Edge> edges, List<Clock> clocks) {
for (Edge e : edges) {
if (!(e.getTarget().getInvariantGuard() instanceof TrueGuard)) {
if (!(e.getTarget().getInvariantGuard() instanceof FalseGuard)) {
CDD target = new CDD(e.getTarget().getInvariantGuard());
CDD target = CDDFactory.createFrom(e.getTarget().getInvariantGuard());
CDD cddBeforeEdge = target.transitionBack(e);
e.setGuard(cddBeforeEdge.conjunction(new CDD(e.getSource().getInvariantGuard())).getGuard(clocks));
CDD sourceInvariantCdd = CDDFactory.createFrom(e.getSource().getInvariantGuard());
e.setGuard(cddBeforeEdge.conjunction(sourceInvariantCdd).getGuard(clocks));
}
}
}
Expand Down Expand Up @@ -225,7 +227,9 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
// calculate and backtrack the part that is NOT inconsistent

CDD incPartOfTransThatSavesUs = new CDD(otherE.getTarget().getInconsistentPart().getPointer());
CDD targetInvariantCDDOfTransThatSavesUs = new CDD(otherE.getTarget().getInvariantGuard());
CDD targetInvariantCDDOfTransThatSavesUs = CDDFactory.createFrom(
otherE.getTarget().getInvariantGuard()
);
CDD goodPart = targetInvariantCDDOfTransThatSavesUs.minus(incPartOfTransThatSavesUs);

CDD doubleCheck = goodPart.transitionBack(otherE);
Expand All @@ -237,7 +241,9 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
assert(doubleCheck.equiv(goodPart));

goodPart = goodPart.past(); // TODO 05.02.21: is it okay to do that?
goodPart = goodPart.conjunction(new CDD(otherE.getSource().getInvariantGuard()));
goodPart = goodPart.conjunction(CDDFactory.createFrom(
otherE.getSource().getInvariantGuard()
));

if (printComments)
Log.debug("Guards done");
Expand All @@ -248,7 +254,8 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
// simply apply guards
CDD cddOfGuard = otherE.getGuardCDD();
cddOfGuard = cddOfGuard.past(); // TODO 05.02.21: IMPORTANT!!!! Since invariants are not bound to start at 0 anymore, every time we use down we need to afterwards intersect with invariant
cddOfGuard = cddOfGuard.conjunction(new CDD(otherE.getSource().getInvariantGuard()));
CDD sourceInvariant = CDDFactory.createFrom(otherE.getSource().getInvariantGuard());
cddOfGuard = cddOfGuard.conjunction(sourceInvariant);
cddThatSavesUs = cddOfGuard.disjunction(cddThatSavesUs);

}
Expand All @@ -257,7 +264,8 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
if (printComments)
Log.debug("Coming to the subtraction");

CDD newIncPart = new CDD(e.getSource().getInvariantGuard()).minus(cddThatSavesUs);
CDD sourceInvariantCdd = CDDFactory.createFrom(e.getSource().getInvariantGuard());
CDD newIncPart = sourceInvariantCdd.minus(cddThatSavesUs);
processSourceLocation(e, newIncPart,passedPairs, inconsistentQueue);


Expand Down Expand Up @@ -285,7 +293,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
CDD incCDD = e.getTarget().getInconsistentPart();

// apply target invariant
CDD invarCDD = new CDD(e.getTarget().getInvariantGuard());
CDD invarCDD = CDDFactory.createFrom(e.getTarget().getInvariantGuard());
incCDD = invarCDD.conjunction(incCDD);

incCDD = incCDD.transitionBack(e);
Expand All @@ -294,7 +302,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 +318,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 All @@ -335,7 +343,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
if (printComments)
Log.debug("Could not be saved by an output");
incCDD = incCDD.past(); // TODO: Check if this works
incCDD = incCDD.conjunction(new CDD(e.getSource().getInvariantGuard()));
incCDD = incCDD.conjunction(CDDFactory.createFrom(e.getSource().getInvariantGuard()));
}

if (printComments)
Expand All @@ -358,13 +366,13 @@ public CDD backExplorationOnTransition(Edge e, CDD incCDD)
incCDD = incCDD.past();

// apply source invariant
CDD invarCDD1 = new CDD(e.getSource().getInvariantGuard());
CDD invarCDD1 = CDDFactory.createFrom(e.getSource().getInvariantGuard());
incCDD = invarCDD1.conjunction(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 All @@ -383,7 +391,9 @@ public static void removeTransitionIfUnsat(Edge e, CDD incCDD, List<Edge> edges


// apply target invariant
CDD tartgetInvCDD= new CDD(e.getTarget().getInvariantGuard());
CDD tartgetInvCDD= CDDFactory.createFrom(
e.getTarget().getInvariantGuard()
);
testForSatEdgeCDD = tartgetInvCDD.conjunction(testForSatEdgeCDD);

testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getTarget().getInconsistentPart());
Expand All @@ -395,15 +405,17 @@ public static void removeTransitionIfUnsat(Edge e, CDD incCDD, List<Edge> edges
CDD guardCDD1 = e.getGuardCDD();
testForSatEdgeCDD = guardCDD1.conjunction(testForSatEdgeCDD);

CDD sourceInvCDD = new CDD(e.getSource().getInvariantGuard());
CDD sourceInvCDD = CDDFactory.createFrom(
e.getSource().getInvariantGuard()
);
testForSatEdgeCDD = sourceInvCDD.conjunction(testForSatEdgeCDD);

// remove inconsistent part

testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getSource().getInconsistentPart());


if (!testForSatEdgeCDD.isNotFalse()) {
if (!testForSatEdgeCDD.notEquivFalse()) {
edges.remove(e);
}
if (printComments)
Expand All @@ -416,7 +428,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 @@ -463,16 +475,20 @@ public static CDD predtOfAllOutputs(Edge e, CDD incCDD, List<Edge> edges)
Log.debug("found an output that might lead us to good");

// Ged invariant Federation
CDD goodCDD = new CDD(otherEdge.getTarget().getInvariantGuard());
CDD goodCDD = CDDFactory.createFrom(
otherEdge.getTarget().getInvariantGuard()
);
goodCDD = goodCDD.minus(otherEdge.getTarget().getInconsistentPart());

// 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());

CDD sourceInvFed = new CDD(otherEdge.getSource().getInvariantGuard());
CDD sourceInvFed = CDDFactory.createFrom(
otherEdge.getSource().getInvariantGuard()
);
goodCDD = sourceInvFed.conjunction(goodCDD);
allGoodCDDs = allGoodCDDs.disjunction(goodCDD);
//Log.debug(incFederation.getZones().get(0).buildGuardsFromZone(clocks));
Expand Down
21 changes: 10 additions & 11 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 @@ -134,7 +133,7 @@ public boolean checkRef() {
if (!checkPreconditions())
return false;

boolean initialisedCdd = CDD.tryInit(allClocks, allBVs);
boolean initialisedCdd = CDDRuntime.tryInit(allClocks, allBVs);

// the first states we look at are the initial ones
waiting.push(getInitialStatePair());
Expand Down Expand Up @@ -185,7 +184,7 @@ public boolean checkRef() {
if (!holds0) {
Log.info("Delay violation");
if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return false;
}
Expand All @@ -196,7 +195,7 @@ public boolean checkRef() {

Log.info("Output violation");
if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return false;
}
Expand All @@ -207,15 +206,15 @@ public boolean checkRef() {
//assert(false); // assuming everything is input enabled
Log.info("Input violation");
if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return false;
}
}

// if we got here it means refinement property holds
if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return true;
}
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
6 changes: 3 additions & 3 deletions 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 Expand Up @@ -327,7 +327,7 @@ public void toJson(String filename)


public SimpleTransitionSystem pruneReachTimed(){
boolean initialisedCdd = CDD.tryInit(clocks.getItems(), BVs.getItems());
boolean initialisedCdd = CDDRuntime.tryInit(clocks.getItems(), BVs.getItems());

//TODO: this function is not correct yet. // FIXED: 05.1.2021
// In the while loop, we should collect all edges associated to transitions (not just all locations associated to states), and remove all that were never associated
Expand Down Expand Up @@ -389,7 +389,7 @@ public SimpleTransitionSystem pruneReachTimed(){
Automaton aut = new Automaton(getName(), locations, edges, getClocks(),getAutomaton().getBVs(), false);

if (initialisedCdd) {
CDD.done();
CDDRuntime.done();
}
return new SimpleTransitionSystem(aut);
}
Expand Down
Loading