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

Guard rename #95

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

Guard rename #95

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
53d08fa
Initial rename
t-lohse Dec 1, 2022
4bb150a
Updated CDD and Grammar naming
t-lohse Dec 1, 2022
2a1e197
Updated tests
t-lohse Dec 1, 2022
9334d41
Pull from main
t-lohse Jan 16, 2023
a268ca3
Some refactor
t-lohse Jan 16, 2023
d118b15
Expression rename
t-lohse Jan 16, 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
14 changes: 7 additions & 7 deletions src/antlr/GuardGrammar.g4 → src/antlr/ExpressionGrammar.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
grammar GuardGrammar;
grammar ExpressionGrammar;

import CommonLexerRules;

@header {
package GuardGrammar;
package ExpressionGrammar;
}

options { caseInsensitive = true; }
Expand All @@ -12,18 +12,18 @@ options { caseInsensitive = true; }
* Parser Rules
*/

guards : guard EOF ;
expressions : expression EOF ;

guard : expression
expression : arithExpression
| or ';'?
| and
;

or : (orExpression OR)+ orExpression;
orExpression : expression | and ;
orExpression : arithExpression | and ;

and : (expression AND)+ expression ;
expression : BOOLEAN | clockExpr | boolExpr | '(' guard ')';
and : (arithExpression AND)+ arithExpression ;
arithExpression : BOOLEAN | clockExpr | boolExpr | '(' expression ')';
clockExpr : VARIABLE ('-'VARIABLE)? OPERATOR '-'? INT ;
boolExpr : VARIABLE OPERATOR BOOLEAN ;

Expand Down
4 changes: 2 additions & 2 deletions src/logic/AggregatedTransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -250,9 +250,9 @@ private boolean containsEdge(Set<Edge> set, Edge edge) {
}

private Edge createEdgeFromTransition(Transition transition, Location source, Location target, Channel channel) {
Guard guard = transition.getGuards(getClocks());
Expression expression = transition.getGuards(getClocks());
t-lohse marked this conversation as resolved.
Show resolved Hide resolved
List<Update> updates = transition.getUpdates();
boolean isInput = getInputs().contains(channel);
return new Edge(source, target, channel, isInput, guard, updates);
return new Edge(source, target, channel, isInput, expression, updates);
}
}
2 changes: 1 addition & 1 deletion src/logic/Bisimilarity.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ public static Automaton checkBisimilarity(Automaton aut1) {

assert (Arrays.equals(Arrays.stream(updates.toArray()).toArray(), Arrays.stream(e.getUpdates().toArray()).toArray()));
}
finalEdges.add(new Edge(l, targetLoc, c, edgeList.get(0).isInput(), allCDDs.getGuard(copy.getClocks()), allEdges.get(0).getUpdates()));
finalEdges.add(new Edge(l, targetLoc, c, edgeList.get(0).isInput(), allCDDs.getExpression(copy.getClocks()), allEdges.get(0).getUpdates()));
}

}
Expand Down
2 changes: 1 addition & 1 deletion src/logic/JsonAutomatonEncoder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ private static JSONObject automatonToJson(Automaton aut){
locationJson.put("y", l.getY());


String guardString =l.getInvariantGuard().toString();
String guardString =l.getInvariant().toString();
/*int i= 0; int j=0;
for (List<Guard> disjunction: l.getInvariant())
{
Expand Down
42 changes: 21 additions & 21 deletions src/logic/Pruning.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ public static SimpleTransitionSystem adversarialPruning(TransitionSystem ts) {

if (initialStateIsInconsistent) {
locations = new ArrayList<>();
locations.add(Location.create("inc", new TrueGuard(), true, false, false, true));
locations.add(Location.create("inc", new TrueExpression(), true, false, false, true));
edges = new ArrayList<>();
}

Expand Down Expand Up @@ -139,11 +139,11 @@ public static void addInconsistentPartsToInvariants(List<Location> locations, Li
if (l.isInconsistent()) {
CDD incCDD = l.getInconsistentPart();
if (incCDD.isUnrestrained()) {
l.setInvariantGuard(new FalseGuard());
l.setInvariant(new FalseExpression());
}
else {
CDD invarMinusIncCDD = new CDD(l.getInvariantGuard()).minus(l.getInconsistentPart());
l.setInvariantGuard(invarMinusIncCDD.getGuard(clocks));
CDD invarMinusIncCDD = new CDD(l.getInvariant()).minus(l.getInconsistentPart());
l.setInvariant(invarMinusIncCDD.getExpression(clocks));
}
}
}
Expand All @@ -156,11 +156,11 @@ public static void addInconsistentPartsToInvariants(List<Location> locations, Li
*/
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());
if (!(e.getTarget().getInvariant() instanceof TrueExpression)) {
if (!(e.getTarget().getInvariant() instanceof FalseExpression)) {
CDD target = new CDD(e.getTarget().getInvariant());
CDD cddBeforeEdge = target.transitionBack(e);
e.setGuard(cddBeforeEdge.conjunction(new CDD(e.getSource().getInvariantGuard())).getGuard(clocks));
e.setGuard(cddBeforeEdge.conjunction(new CDD(e.getSource().getInvariant())).getExpression(clocks));
}
}
}
Expand Down Expand Up @@ -200,14 +200,14 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
CDD guardCDD = e.getGuardCDD();
CDD fedAfterRemovingInconsistentPart =guardCDD.minus(target);

e.setGuard(fedAfterRemovingInconsistentPart.getGuard(clocks));
e.setGuard(fedAfterRemovingInconsistentPart.getExpression(clocks));
}

// Removing the transition / strenthening the guards might have turned the source location inconsistent
// This happens if there is an invariant, and part of the invariant cannot delay to enable an output anymore

// if there is no invariant, there cannot be a deadlock, and we do not care about whether there is any input or outputs leaving
if (e.getSource().getInvariantGuard() instanceof TrueGuard) {
if (e.getSource().getInvariant() instanceof TrueExpression) {
if (printComments)
Log.debug("Source has no invariant, nothing more to do");
} else {
Expand All @@ -225,7 +225,7 @@ 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 = new CDD(otherE.getTarget().getInvariant());
CDD goodPart = targetInvariantCDDOfTransThatSavesUs.minus(incPartOfTransThatSavesUs);

CDD doubleCheck = goodPart.transitionBack(otherE);
Expand All @@ -237,7 +237,7 @@ 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(new CDD(otherE.getSource().getInvariant()));

if (printComments)
Log.debug("Guards done");
Expand All @@ -248,7 +248,7 @@ 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()));
cddOfGuard = cddOfGuard.conjunction(new CDD(otherE.getSource().getInvariant()));
cddThatSavesUs = cddOfGuard.disjunction(cddThatSavesUs);

}
Expand All @@ -257,7 +257,7 @@ 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 newIncPart = new CDD(e.getSource().getInvariant()).minus(cddThatSavesUs);
processSourceLocation(e, newIncPart,passedPairs, inconsistentQueue);


Expand Down Expand Up @@ -285,7 +285,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 = new CDD(e.getTarget().getInvariant());
incCDD = invarCDD.conjunction(incCDD);

incCDD = incCDD.transitionBack(e);
Expand Down Expand Up @@ -335,7 +335,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(new CDD(e.getSource().getInvariant()));
}

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

// apply source invariant
CDD invarCDD1 = new CDD(e.getSource().getInvariantGuard());
CDD invarCDD1 = new CDD(e.getSource().getInvariant());
incCDD = invarCDD1.conjunction(incCDD);

if (printComments)
Expand All @@ -383,7 +383,7 @@ public static void removeTransitionIfUnsat(Edge e, CDD incCDD, List<Edge> edges


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

testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getTarget().getInconsistentPart());
Expand All @@ -395,7 +395,7 @@ 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 = new CDD(e.getSource().getInvariant());
testForSatEdgeCDD = sourceInvCDD.conjunction(testForSatEdgeCDD);

// remove inconsistent part
Expand Down Expand Up @@ -463,7 +463,7 @@ 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 = new CDD(otherEdge.getTarget().getInvariant());
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
Expand All @@ -472,7 +472,7 @@ public static CDD predtOfAllOutputs(Edge e, CDD incCDD, List<Edge> edges)
goodCDD = goodCDD.transitionBack(otherEdge);
//goodCDD = CDD.applyReset(goodCDD, otherEdge.getUpdates());

CDD sourceInvFed = new CDD(otherEdge.getSource().getInvariantGuard());
CDD sourceInvFed = new CDD(otherEdge.getSource().getInvariant());
goodCDD = sourceInvFed.conjunction(goodCDD);
allGoodCDDs = allGoodCDDs.disjunction(goodCDD);
//Log.debug(incFederation.getZones().get(0).buildGuardsFromZone(clocks));
Expand Down
14 changes: 7 additions & 7 deletions src/logic/SimpleTransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,16 +125,16 @@ public boolean checkMovesOverlap(List<Transition> trans) {

if (state1.getInvariant().isNotFalse() && state2.getInvariant().isNotFalse()) {
if(state1.getInvariant().intersects(state2.getInvariant())) {
Log.debug(trans.get(i).getGuardCDD().getGuard(clocks.getItems()));
Log.debug(trans.get(j).getGuardCDD().getGuard(clocks.getItems()));
Log.debug(trans.get(i).getGuardCDD().getExpression(clocks.getItems()));
Log.debug(trans.get(j).getGuardCDD().getExpression(clocks.getItems()));
Log.debug(trans.get(0).getEdges().get(0).getChannel());
Log.debug(trans.get(0).getEdges().get(0));
Log.debug(trans.get(1).getEdges().get(0));
Log.debug(state1.getInvariant().getGuard(clocks.getItems()));
Log.debug(state2.getInvariant().getGuard(clocks.getItems()));
Log.debug(state1.getInvariant().getExpression(clocks.getItems()));
Log.debug(state2.getInvariant().getExpression(clocks.getItems()));
trans.get(j).getGuardCDD().printDot();
Log.debug(trans.get(i).getEdges().get(0).getGuardCDD().getGuard(clocks.getItems()));
Log.debug(trans.get(j).getEdges().get(0).getGuardCDD().getGuard(clocks.getItems()));
Log.debug(trans.get(i).getEdges().get(0).getGuardCDD().getExpression(clocks.getItems()));
Log.debug(trans.get(j).getEdges().get(0).getGuardCDD().getExpression(clocks.getItems()));
Log.debug("they intersect??!");
return true;
}
Expand Down Expand Up @@ -269,7 +269,7 @@ private boolean passedContainsState(State state1) {


for (State passedState : passed) {
Log.debug(" " + passedState.getLocation() + " " + passedState.getInvariant().getGuard(clocks.getItems()));
Log.debug(" " + passedState.getLocation() + " " + passedState.getInvariant().getExpression(clocks.getItems()));
if (state.getLocation().equals(passedState.getLocation()) &&
state.getInvariant().isSubset((passedState.getInvariant()))) {
return true;
Expand Down
6 changes: 3 additions & 3 deletions src/logic/State.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ public CDD getLocationInvariant() {
return location.getInvariantCdd();
}

public Guard getInvariants(List<Clock> relevantClocks) {
return location.getInvariantCdd().getGuard(relevantClocks);
public Expression getInvariants(List<Clock> relevantClocks) {
t-lohse marked this conversation as resolved.
Show resolved Hide resolved
return location.getInvariantCdd().getExpression(relevantClocks);
}

// TODO: I think this is finally done correctly. Check that that is true!
Expand Down Expand Up @@ -121,7 +121,7 @@ public void extrapolateMaxBoundsDiag(HashMap<Clock,Integer> maxBounds, List<Cloc
if (copy.toString().contains("30"))
{
Log.debug("max bounds : " + maxBounds);
Log.debug(copy.getGuard(relevantClocks));
Log.debug(copy.getExpression(relevantClocks));
print = true;
}
if (copy.isBDD())
Expand Down
6 changes: 3 additions & 3 deletions src/logic/StatePair.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,13 @@ public void setNode(GraphNode node) {
* This function prints the <code>StatePair</code> in a more readable manner compared to <code>toString</code>.
* <p>
* The format of the function is <p>
* <code>(LEFT_LOCATION, RIGHT_LOCATION) [ GUARD ]</code>
* <code>(LEFT_LOCATION, RIGHT_LOCATION) [ EXPRESSION ]</code>
* </p>whereas the format of <code>toString</code> is <p>
* <code>L=(LEFT_LOCATION, RIGHT_LOCATION) CDD= LEFT_INVARIANT RIGHT_INVARIANT</code>
* </p>
* </p>
* <p>
* This function prints the zone as a guard, not a <code>CDD</code> or <code>DBM</code>.
* This function prints the zone as an expression, not a <code>CDD</code> or <code>DBM</code>.
* </p>
* <p>
* Since <code>left.getInvariant()</code> is equal to <code>right.getInvariant()</code>,
Expand All @@ -52,7 +52,7 @@ public void setNode(GraphNode node) {
public String prettyPrint() {
return String.format("(%s %s) [ %s ]",
left.getLocation(), right.getLocation(),
left.getInvariant().getGuard().prettyPrint());
left.getInvariant().getExpression().prettyPrint());
}

@Override
Expand Down
2 changes: 1 addition & 1 deletion src/logic/Transition.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ public List<Edge> getEdges() {
return move.getEdges();
}

public Guard getGuards(List <Clock> relevantClocks ) {
public Expression getGuards(List <Clock> relevantClocks ) {
t-lohse marked this conversation as resolved.
Show resolved Hide resolved
return move.getGuards( relevantClocks);
}

Expand Down
Loading