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

Fix/inconsistent location invariant #94

Merged
merged 19 commits into from
Mar 9, 2023
Merged

Fix/inconsistent location invariant #94

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
44ba969
chore: Added the quotient clock to the location invariant
Brandhoej Nov 29, 2022
c425e4d
fix: Automaton makeInputEnabled terminal error
Brandhoej Nov 29, 2022
2d6c8fe
tests: Added more tests for Location
Brandhoej Nov 29, 2022
8c4e975
fix: ConsistencyTest now works consistenly
Brandhoej Nov 29, 2022
ceeb7b0
test: testFromFramework4 now runs
Brandhoej Nov 29, 2022
d640aaf
merge with main
Brandhoej Jan 3, 2023
13f3f4a
feature(CDD): Optimisations for CDDs and terminal reduce fix
Brandhoej Jan 16, 2023
4426701
merge with main
Brandhoej Jan 16, 2023
87ede64
wip
Brandhoej Feb 1, 2023
b90279a
pr changes
Brandhoej Feb 5, 2023
ea2d015
doc: added comment for hardcopy usage
Brandhoej Feb 12, 2023
20ec70e
refactor: Missing curly and change container if
Brandhoej Feb 12, 2023
ea490ef
doc: Removed empty java doc
Brandhoej Feb 12, 2023
234bde8
removed /bin
Brandhoej Feb 12, 2023
622ea3f
fix: transitionback cddlib crash if this or update is terminal
Brandhoej Feb 12, 2023
e78395c
fix(CDD): Some dirty flags were incorrect
Brandhoej Mar 9, 2023
006a7d5
Merge branch 'main' into fix/inconsistent_location_invariant
Brandhoej Mar 9, 2023
c17534c
test(Bisim): Ignore one bisimilarity test
Brandhoej Mar 9, 2023
1b14d0c
refactor: minor corrections
Brandhoej Mar 9, 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
1 change: 1 addition & 0 deletions bin/default
Open in desktop
Submodule default added at ceeb7b
2 changes: 1 addition & 1 deletion src/logic/AggregatedTransitionSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ private Automaton aggregate(Automaton[] automata) {
String targetName = targetState.getLocation().getName();
locationMap.computeIfAbsent(
targetName, key -> {
Location newLocation = Location.createFromState(targetState, clocks.getItems());
Location newLocation = Location.createFromState(targetState);
locations.add(newLocation);
return newLocation;
}
Expand Down
10 changes: 5 additions & 5 deletions src/logic/Quotient.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ public String getName() {
@Override
public List<Move> getNextMoves(Location location, Channel a) {
Location univ = Location.createUniversalLocation("universal", 0, 0);
Location inc = Location.createInconsistentLocation("inconsistent", 0, 0);
Location inc = Location.createInconsistentLocation("inconsistent", 0, 0, newClock);

List<Move> resultMoves = new ArrayList<>();

Expand Down Expand Up @@ -94,7 +94,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
// Rule 1 (cartesian product)
if (in(a, intersect(s.getActions(), t.getActions()))) {
Log.debug("Rule 1");
List<Move> moveProduct = moveProduct(t_moves, s_moves, true,true);
List<Move> moveProduct = moveProduct(t_moves, s_moves, true, true);
for (Move move : moveProduct) {
move.conjunctCDD(move.getEnabledPart());
}
Expand All @@ -105,7 +105,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
if (in(a, difference(s.getActions(), t.getActions()))) {
Log.debug("Rule 2");
List<Move> movesLeft = new ArrayList<>();
movesLeft.add(new Move(lt,lt, new ArrayList<>()));
movesLeft.add(new Move(lt, lt, new ArrayList<>()));

List<Move> moveProduct = moveProduct(movesLeft, s_moves, true, true);
for (Move move : moveProduct) {
Expand Down Expand Up @@ -176,8 +176,8 @@ public List<Move> getNextMoves(Location location, Channel a) {
if (in(a, difference(t.getActions(), s.getActions()))) {
Log.debug("Rule 8");
List<Move> movesRight = new ArrayList<>();
movesRight.add(new Move(ls,ls,new ArrayList<>()));
List<Move> moveProduct = moveProduct(t_moves, movesRight, true,true);
movesRight.add(new Move(ls, ls, new ArrayList<>()));
List<Move> moveProduct = moveProduct(t_moves, movesRight, true, true);
for (Move move : moveProduct) {
move.conjunctCDD(move.getEnabledPart());
}
Expand Down
5 changes: 3 additions & 2 deletions src/logic/Refinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -432,8 +432,9 @@ private boolean checkActions(State state1, State state2, boolean isInput) {
Log.debug("create pairs failed");
if (RET_REF)
{
Location ll = Location.createInconsistentLocation("inconsistent", 0, 0);
Location rl = Location.createInconsistentLocation("inconsistent", 0, 0);
Clock inconsistentClock = new Clock("inconsistent clock", "refinement");
Brandhoej marked this conversation as resolved.
Show resolved Hide resolved
Location ll = Location.createInconsistentLocation("inconsistent", 0, 0, inconsistentClock);
Location rl = Location.createInconsistentLocation("inconsistent", 0, 0, inconsistentClock);
StatePair refViolationStates = new StatePair(new State(ll,CDD.cddTrue()), new State(rl, CDD.cddTrue()));
currNode.constructSuccessor(refViolationStates, leaderEdges, followerEdges);
}
Expand Down
50 changes: 31 additions & 19 deletions src/models/Automaton.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,30 +268,42 @@ public int hashCode() {
public void makeInputEnabled() {
boolean initialisedCdd = CDD.tryInit(clocks, BVs);

for (Location loc : getLocations()) {
CDD sourceInvariantCDD = loc.getInvariantCdd();
// loop through all inputs
for (Location location : getLocations()) {
CDD invariant = location.getInvariantCdd();

for (Channel input : getInputAct()) {
// The part which is already handled by existing edges.
CDD enabledPart = CDD.cddFalse();
// The part which requires an edge to be input enabled.
CDD disabledPart = invariant;

// Calculate the enabled CDD.
List<Edge> edges = getEdgesFromLocationAndSignal(location, input);
if (!edges.isEmpty()) {
for (Edge edge : edges) {
Brandhoej marked this conversation as resolved.
Show resolved Hide resolved
CDD targetInvariant = edge.getTarget().getInvariantCdd();
CDD preGuard = targetInvariant.transitionBack(edge);
enabledPart = enabledPart.disjunction(preGuard);
}

// build CDD of zones from edges
List<Edge> inputEdges = getEdgesFromLocationAndSignal(loc, input);
CDD resCDD;
CDD cddOfAllEdgesWithCurrentInput = CDD.cddFalse();
if (!inputEdges.isEmpty()) {
for (Edge edge : inputEdges) {
CDD target = edge.getTarget().getInvariantCdd();
CDD preGuard1 = target.transitionBack(edge);
cddOfAllEdgesWithCurrentInput = cddOfAllEdgesWithCurrentInput.disjunction(preGuard1);
if (enabledPart.isTerminal()) {
continue;
}
Brandhoej marked this conversation as resolved.
Show resolved Hide resolved
cddOfAllEdgesWithCurrentInput = cddOfAllEdgesWithCurrentInput.removeNegative().reduce();
// subtract the federation of zones from the original fed
resCDD = sourceInvariantCDD.minus(cddOfAllEdgesWithCurrentInput);
} else {
resCDD = sourceInvariantCDD;
}

if (resCDD.isNotFalse()) {
Edge newEdge = new Edge(loc, loc, input, true, resCDD.getGuard(getClocks()), new ArrayList<>());
// If the enabled part is true then the disabled part will be false
Brandhoej marked this conversation as resolved.
Show resolved Hide resolved
if (enabledPart.isTrue()) {
continue;
}

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

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