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

Additional timelock check #148

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Additional timelock check #148

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
154585b
added a test for timelock
Sven-Schneider Jan 29, 2021
98c0cbe
added outputs for explanation
Sven-Schneider Jan 29, 2021
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
28 changes: 28 additions & 0 deletions prism/src/pta/ForwardsReach.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,18 +181,37 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs
throw new PrismException(s);
}
}
boolean found_some_transition_guaranteed_to_be_enabled = false;
// For each outgoing transition...
for (Transition transition : pta.getTransitions(lz.loc)) {
dests = new int[transition.getNumEdges()];
boolean enabled = false;
boolean unenabled = false;
Edge unenabledEdge = null;
count = 0;
boolean found_some_edge_not_enabled = false;
for (Edge edge : transition.getEdges()) {
// Do "discrete post" for this edge
// (followed by c-closure)
lz2 = lz.deepCopy();
System.out.println("\nSS1: "+lz2);
lz2.dPost(edge);
System.out.println("SS2: "+lz2);
{
LocZone lz3 = lz2.deepCopy();
System.out.println("SS3: "+lz3);
lz3.dPre(edge);
System.out.println("SS4: "+lz3);
NCZone complement=lz3.zone.createComplement();
System.out.println("SS4b: "+complement);
complement.addConstraints(transition.getGuardConstraints());
System.out.println("SS5: "+complement);
complement.intersect(lz.zone);
System.out.println("SS6: "+complement);
if (!complement.isEmpty()) {
found_some_edge_not_enabled = true;
}
}
lz2.cClosure(pta);
// If non-empty, create edge, also adding state to X if new
if (!lz2.zone.isEmpty()) {
Expand Down Expand Up @@ -220,7 +239,16 @@ private ReachabilityGraph buildForwardsGraphFormats10(PTA pta, BitSet targetLocs
}
graph.addTransition(src, transition, dests, null);
}
if (!found_some_edge_not_enabled) {
found_some_transition_guaranteed_to_be_enabled = true;
}
}
if (!pta.getTransitions(lz.loc).isEmpty() && !found_some_transition_guaranteed_to_be_enabled) {
throw new PrismException(
"Badly formed PTA at location " + pta.getLocationNameString(lz.loc) + " when " + lz.zone +
" has exiting transitions but all may be disabled " +
"by the invariants of some of their targets.");
}
// Check for another possible cause of timelock:
// no PTA transitions *enabled* and not possible for time to diverge
// (NB: This should be defunct now because of earlier timelock check)
Expand Down