Skip to content
Snippets Groups Projects
Commit f9cab654 authored by tempiaa's avatar tempiaa
Browse files

Code cleaning

parent 93a1ac79
No related branches found
No related tags found
1 merge request!325Avatar model-checker improvements
...@@ -71,7 +71,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { ...@@ -71,7 +71,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private Map<Integer, SpecificationState> states; private Map<Integer, SpecificationState> states;
private Map<Long, SpecificationState> statesByID; private Map<Long, SpecificationState> statesByID;
private List<SpecificationState> pendingStates; private List<SpecificationState> pendingStates;
private List<SpecificationState> allPendingStates;
//private List<SpecificationLink> links; //private List<SpecificationLink> links;
private int nbOfLinks; private int nbOfLinks;
private long stateID = 0; private long stateID = 0;
...@@ -451,7 +450,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { ...@@ -451,7 +450,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
states = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>()); states = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>());
statesByID = Collections.synchronizedMap(new HashMap<Long, SpecificationState>()); statesByID = Collections.synchronizedMap(new HashMap<Long, SpecificationState>());
pendingStates = Collections.synchronizedList(new LinkedList<SpecificationState>()); pendingStates = Collections.synchronizedList(new LinkedList<SpecificationState>());
allPendingStates = Collections.synchronizedList(new LinkedList<SpecificationState>());
//links = Collections.synchronizedList(new ArrayList<SpecificationLink>()); //links = Collections.synchronizedList(new ArrayList<SpecificationLink>());
nbOfLinks = 0; nbOfLinks = 0;
...@@ -621,7 +619,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { ...@@ -621,7 +619,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
go = false; go = false;
} else { } else {
// Handle one given state // Handle one given state
allPendingStates.add(s);
computeAllStatesFrom(s); computeAllStatesFrom(s);
// Release the computation // Release the computation
releasePickupState(s); releasePickupState(s);
...@@ -1617,7 +1614,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { ...@@ -1617,7 +1614,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//found a branch with false liveness //found a branch with false liveness
propertyDone = true; propertyDone = true;
livenessInfo.result = false; livenessInfo.result = false;
} else if (stateIsReachableFromState(similar, _ss)) { //TODO: concurrent operation when going through the next list } else if (stateIsReachableFromState(similar, _ss)) {
//found a loop with false liveness //found a loop with false liveness
propertyDone = true; propertyDone = true;
livenessInfo.result = false; livenessInfo.result = false;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment