diff --git a/doc/avatarmodelchecker/images/modelcheckerwindow.png b/doc/avatarmodelchecker/images/modelcheckerwindow.png
index d6fd7e1886348debc06536e6ed42dfc0d8f61c84..ae361537df1c17b2ff6deedc1d6ec13e3fbba60c 100644
Binary files a/doc/avatarmodelchecker/images/modelcheckerwindow.png and b/doc/avatarmodelchecker/images/modelcheckerwindow.png differ
diff --git a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
index fb75f9cf16170e8fc40a61ce66ad2879fd42233e..f427cd3a63b737d9fffdb765855500d0e63346db 100644
--- a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
+++ b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
@@ -235,6 +235,7 @@ To start the CTL query verification, let's compile again and let's open the mode
In this section we will explain all the features and options that are present in the AVATAR model-checker. For a reference to the model-checking window, please refer to figure \ref{fig:mcwindow}.
\\\\The model-checker allows to generate a reachability graph and to prove properties. Starting from the top, the first section contains graph generations options. In particular:
\begin{itemize}
+ \item \textbf{Word size}: the words can be represented on 32, 16 or 8 bits.
\item \textbf{Do not display empty transitions as internal states}: in the reachability graph generation, states are not created for empty transitions (no action, no time, no choice). In practice, empty transition states are collapsed together. This option does not affect the verification. Option on by default.
\item \textbf{Ignore concurrency between internal actions}: this option allows to ignore a full concurrency study. It is very useful to limit the state explosion of the model due to all the concurrencies among its states. It is so suggested to keep it selected to have a faster verification. This option, however, affects only in the \textit{leadsto} study, and the reachability graph generation. \textbf{Important}: basic concurrency it is evaluated also with this optimization selected. Basic concurrency means that concurrency is normally evaluated until states with multiple transitions, or if statement, or signals communication are encounted. In normal usage, you should not need to deselect this option (example in the next section \ref{sec:cb}). Option on by default.
\item \textbf{Ignore states between internal actions}: This option allows to ignore intermediate states between actions that can be directly executed. this optimization helps decreasing the number of states in the reachability graph generation. If \textit{Ignore concurrency between internal actions} is not selected, this option automatically deactivated. We suggest to keep this option selected for verification as it would not affect the result. Option on by default.
@@ -245,6 +246,7 @@ The next section contains options for basic properties verification:
\begin{itemize}
\item \textbf{No deadlocks}: it checks that the model is deadlock free
\item \textbf{Reinitialization}: it checks that, for all the paths, the model will eventually restart to the initial state
+ \item \textbf{No internal action loops}: it checks that in states machines, there are not possible infinite loops which have no interractions (signal communications) with the environment (other blocks). This check helps to detect if a system stops interracting with the environment during its execution.
\item \textbf{Reachability}: it checks for states reachability
\item \textbf{Liveness}: it checks for states liveness
\end{itemize}
@@ -261,11 +263,16 @@ The query syntax for CTL formulas, for expressions \texttt{p} and \texttt{q}, is
\item \textbf{E<> p}: there exists a path in which property p will eventually be true (other common notation \textbf{EF p})
\item \textbf{p --> q}: whenever p is true, then q will eventually be true at some subsequent moment (other common notation \textbf{G(p $\Rightarrow$ Fq)})
\end{itemize}
-Expression \texttt{p} and \texttt{q} may be on states or variables. The format used to reference a variable or a state of a block is \textit{BlockName.AttributeName} or \textit{BlockName.StateName}. Conditions on variables can be combined using classic C code like boolean operators (||, \&\&, and, or). Variables can be negated or inverted (not(variable)). Examples:
+Expression \texttt{p} and \texttt{q} may contain condition on states and/or variables. The format used to reference a variable or a state of a block is \textit{BlockName.AttributeName} or \textit{BlockName.StateName}. Conditions on variables can be combined using classic boolean (||, \&\&, and, or) and integer (==, >, >=, <, <=, +, -, *, /) operators. Variables can be negated or inverted (not(var), !(var), -var). States are considered as a boolean variable.
+\\\\
+Before the pragma, the letter \textit{T} or \textit{F} may be inserted to specify if the expected result of the pragma is true, in the former case, or false, in the latter. The pragma will be considered satisfied if the result is equivalent to the expected one.
+\\\\
+Here there are few examples of valid pragmas:
\begin{itemize}
\item \textit{E<> Passenger.isInCockpit ==true \&\& DoorAndLockButton.inside==1}: there exists a path in which there is at least one state in which Passenger.isInCockpit is true and DoorAndLockButton.inside is equal to 1
- \item \textit{A[] MainController.currentPressure < 25}: MainController.currentPressure is always less than 25
+ \item \textit{F A[] MainController.currentPressure < 25}: MainController.currentPressure is always less than 25. The expected result is false.
\item \textit{DoorAndLockButton.IN\_EMERGENCY\_CALL --> DoorAndLockButton.CLOSED\_AND\_LOCKED || DoorAndLockButton.CLOSED\_AND\_UNLOCKED}: whenever DoorAndLockButton.IN\_EMERGENCY\_CALL state is encounted, then or DoorAndLockButton.CLOSED\_AND\_LOCKED or DoorAndLockButton.CLOSED\_AND\_UNLOCKED will be encounted at some subsequent moment.
+ \item \textit{T A<> Sensor.iter == Main.dataSize - 1}: all the paths reach the condition where Sensor.iter is equal to Main.dataSize - 1.
\end{itemize}
\subsection{Traces generation} \label{sec:tg}
@@ -275,8 +282,9 @@ For advanced verification queries and deadlock check, there is the possibility o
\item \textbf{A<> p}: shows the path that disproves the property
\item \textbf{E[] p}: shows the path that proves the property
\item \textbf{E<> p}: shows the path that proves the property
-\item \textbf{p --> q}: shows the path that disproves the property starting from a state with p valid.
+\item \textbf{p --> q}: shows the path that disproves the property starting from a state with p valid
\item \textbf{No deadlocks?}: shows a path to a deadlock
+\item \textbf{No internal action loops?}: shows an infinite loop that has no interraction with the environment
\end{itemize}
The \textbf{Generate property AUT graphs trace} option allows us to display the propery traces as a reachability graph, saving it in AUT format. An entry to the graph, with the name of the query, will appear in the \textit{R. Graphs} section in TTool.
\\\\
@@ -434,6 +442,12 @@ For nonempty transitions, in general, the execution procedure is the same as the
\section{Reachability of States}
The reachability condition of states is checked while creating the reachability graph. The array \texttt{reachabilities} contains the states elements to be checked. Every time a transition is executed, from state $s_t$ to state $s_{t+1}$, $s_{t+1}$ is checked for reachability. When all the states elements in \texttt{reachabilities} have been reached or the reachability graph is completed, the reachability study finishes.
+\subsection{Deadlocks}
+Deadlocks are searched while building the reachability graph. If a state with no available transitions is encountered, the model-checker is stopped using the flag \textit{propertyDone}. The deadlock study is bypassed if another previous study finds deadlocks.
+
+\subsection{Reinitialization}
+The model-checker contains an option to test if the system always reaches the initial state for each execution trace. This is verified as a liveness of the \textit{State 0} represented by \texttt{SpecificationReinit}.
+
\section{Safety and Liveness}
\subsection{Definitions}
In the model also safety and liveness conditions could be proved. In particular, imagining a structure in time of the model, as a tree, the following CTL and LTL formulas are supported:
@@ -442,25 +456,56 @@ In the model also safety and liveness conditions could be proved. In particular,
\item \textbf{A<> p}: property p will eventually be true for each path (other common notation \textbf{AF p})
\item \textbf{E[] p}: there exists at least one path in which property p is always true (other common notation \textbf{EG p})
\item \textbf{E<> p}: there exists a path in which property p will eventually be true (other common notation \textbf{EF p})
- \item \textbf{p --> q}: whenever p is true, then q will be true at some subsequent moment (other common notation \textbf{G(p $\Rightarrow$ Fq}))
+ \item \textbf{p --> q}: whenever p is true, then q will be true at some subsequent moment (other common notation \textbf{G(p $\Rightarrow$ Fq}) called \textit{leadsTo})
\end{itemize}
with \textit{p} and \textit{q} properties. \textbf{Properties are written as expressions on variables or states of the AVATAR model}.
\subsection{Handling of safety and liveness properties by the AVATAR model checker}
-Safety and liveness properties are represented by the \texttt{SafetyProperty} class. The properties are built in the AvatarExpressionSolver class. It creates a syntax tree where each leaf is a AvatarExpressionAttribute or an immediate value and each node is an operator. An AvatarExpressionAttribute can represent a state or a variable of the model. It contains pointers so that, given a state of the model checker, it extracts the associated value in \textit{O(1)}. It can represent integers and boolean values encoded as integers. So, results of properties can be extracted just by visiting the AvatarExpressionSolver tree. AvatarExpressionSolver is also used for guards and actions. The methods \texttt{getSolverResult(SpecificationState)} and \texttt{getSolverResult(SpecificationState, AvatarStateMachineElement)} can be use to obtain the expressions result.\\
-
-Safety properties are solved by finding loops or terminal conditions (deadlocks) in the model. For each property type we now explain how the modelchecker behaves.
+Safety and liveness properties are represented by the \texttt{SafetyProperty} class. The properties are built in the AvatarExpressionSolver class. It creates a syntax tree where each leaf is an AvatarExpressionAttribute or an immediate value and each node is an operator. An AvatarExpressionAttribute can represent a state or a variable of the model. It contains pointers so that, given a state of the model checker, it extracts the associated value in \textit{O(1)}. It can represent integers and boolean values encoded as integers. So, results of properties can be extracted just by visiting the AvatarExpressionSolver tree. AvatarExpressionSolver is also used for guards and actions. The methods \texttt{getSolverResult(SpecificationState)} and \texttt{getSolverResult(SpecificationState, AvatarStateMachineElement)} can be used to obtain the expressions result.
+\\\\
+Safety properties are solved by finding loops or terminal conditions (deadlocks) in the model. For each property type we now explain how the modelchecker behaves:
\begin{itemize}
- \item \textbf{A[] p}: if during the reachability graph creation, $p$ is false is a new state new state has p false, then the property is false.
+ \item \textbf{A[] p}: if during the reachability graph creation a new state has $p$ false, then the property is false.
\item \textbf{A<> p}: if the property is true for a state, stop the search on that path. If a false loop or a false deadlock is found, the property is false. If no false loops or false deadlocks are found, the property is true.
\item \textbf{E[] p}: if the property is false for a state, stop the search on that path. If a true loop or a true deadlock is found , the property is true. If no true loops or false deadlocks are found, the property is false.
\item \textbf{E<> p}: if during the reachability graph creation, $p$ is true in a new state, then the property is true.
- \item \textbf{p --> q}: every time \texttt{p} is true save the SpecificationState in the safetyLeadStates array. Then, for each node in safetyLeadStates start a liveness check \texttt{A<>p} from that node. If the liveness is true for all the nodes in safetyLeadStates or safetyLeadStates is empty, the property is true, else it is false.
+ \item \textbf{p --> q}: every time \texttt{p} is true, save the SpecificationState in the \textit{safetyLeadStates} array. Then, for each node in \textit{safetyLeadStates} start a liveness check \texttt{A<> q} from that node. If the liveness is true for all the nodes in safetyLeadStates or safetyLeadStates is empty, the property is true, else it is false. The model-checking is bounded in order to reduce the exploration space in case of false pragmas. It allows also to prove false properties on infinite graphs. The bound is defined on the number of states matching property \texttt{p} in the current execution. When the number of states is greater than a threshold, the model-checker is paused, the current situation is saved, and the verification of \textit{q} starts from the retrieved states. If the property cannot be proved by these states, the model-checker on \textit{p} is resumed and a new grater threshold is defined.
+\end{itemize}
+The main methods involved in the properties verification process are:
+\begin{itemize}
+ \item \texttt{executeSafetyRun}: it executes a safety property and it retrieves the result on the current model. It has options to ignoreConcurrence, emptyTransitions and to use partialHashing in the leadsTo verification (more details in the internal action loops section \ref{sec:il}).
+ \item \texttt{evaluateSafetyOfProperty}: given the current and old state, this method checks if the property is satisfied, still satisfied or not satisfied. It returns the result which is assigned to the flag \textit{property} of a SpecificationState.
+ \item \texttt{actionOnProperty}: it selects an action based on the type of verification, the current result of the property, and if the node exists already (possible loop). If the general result can be concluded, the flag \textit{propertyDone} is set to stop the execution of the model-checker.
+ \item \texttt{checkPropertyOnDeadlock}: given the current state with no executable transitions (deadlock), it executes an action depending on the type of CTL query.
\end{itemize}
\subsection{Handling combinatory explosion}
-The exploration space of states explodes easily in many models. That's why proving properties is hard. The basic idea of liveness is to find a counter example to prove it wrong. So, we want to detect a cycle (or a path that ends to a deadlock) for which the state we want to check is not live. If the states space explodes, an exploration in breadth will not be effective as the number of nodes increases too much before proving or disproving any property, the space will be too big to be explored.\\
+The exploration space of states explodes easily in many models. That's why proving properties is hard. The basic idea of liveness is to find a counterexample to prove it wrong. So, we want to detect a cycle (or a path that ends to a deadlock) for which the state we want to check is not live. If the states space explodes, an exploration in breadth will not be effective as the number of nodes increases too much before proving or disproving any property, the space will be too big to be explored.
+\\\\
+Moreover, loops are found analyzing a path in depth. So, the check is executed in a depth first search-like manner, instead of a breadth first search implemented for other types of studies, like reachability. It will allow us to search through a path for a property to be true or false having a result within a manageable state-space most of the time. As soon as a property is (un)satisfied the search can continue through another path or stop. In the implementation, each thread follows a path to disprove the liveness. As soon as the property is unsatisfied, the check can stop. As soon as the property is satisfied, the search in that path can stop, and another one is fetched.
+\\\\
+To limit the state's explosion, it is advisable to merge action nodes when possible. This happens inside the method \textit{computeAllInternalStatesFrom} where all the possible executable action transitions are executed and merged into one state. During the \textit{leadsTo} verification also \textit{reduceCombinatorialExplosionProperty} is also used to execute and merge transitions keeping a property valid in order to reduce the number of states added in the structure \textit{safetyLeadStates}.
-Moreover, loops are found analyzing a path in depth. So, the check is executed in a depth first search-like manner, instead of a breadth first search implemented for other types of studies, like reachability. It will allow us to search through a path for a property to be true or false having a result within a manageable states space most of the times. As soon as a property is (un)satisfied the search can continue through another path or stop. In the implementation, each thread follows a path to disprove the liveness. As soon as the property is unsatisfied, the check can stop. As soon as the property is satisfied, the search in that path can stop, and another one is fetched.\\
+\section{Internal action loops} \label{sec:il}
+Internal action loops are used to check conditions when the system stops interracting with the environment. This condition may happen when there are action loops, which do not contain any signal communication, in the state machine of the blocks. If a state machine contains this type of loops, we want to verify that an exit condition is always reached (live).
+\\\\
+The internal loops are detected statically through a strong connected components search executed by the method \texttt{checkStaticInternalLoops} in the AvatarStateMachine class. The method returns a list of all the action loops which are described by a list of transitions.
+\\\\
+The verification of internal action loops is then managed in the \textit{SpecificationActionLoop} class. The check is verified using a \textit{leadsTo} pragma built as follows:
+\begin{itemize}
+ \item if no static loops are detected, a block is free from internal action loops
+ \item if the loops contains transitions from a random block, the loop is removed as the exit condition is guaranteed by construction
+ \item all the states contained in the loops are collected
+ \item a \textit{leadsTo} query \textbf{p --> q} is built with \textbf{p} equal to the logic \textit{OR} of all the states collected and with \textbf{q} equal to the not of \textbf{p}. This pragma verifies that once entered into a state contained in a possible action loop, in a subsequent moment, a state not contained in a action loop is always reached.
+ \item the pragma is verified by the model-checker. If the result is false, the block contains at least one infinite action loop trace
+ \item these operations are repeated for each block in the system
+\end{itemize}
+For instance, if a static loop contains the states \textit{Collect, Elaborate, Fail, Retry} the pragma created would be \textit{Collect || Elaborate || Fail || Retry --> !(Collect || Elaborate || Fail || Retry)}.
+\section{Verification traces}
+Verification traces are extracted using the class \textit{CounterexampleTrace}. For each state created during the model-checking a \textit{CounterexampleTraceState} is associated with it to save the current state pointer for each block and a pointer to a father. All the "counter" states are inserted in the map \textit{traceStates}. The final verification state is extracted by the method \textit{evaluateSafetyOfProperty} or \textit{checkPropertyOnDeadlock}. That state represents a point of a loop, of a deadlock, or a reachability.
+\\\\
+The verification trace is constructed in the \textit{CounterexampleTrace} class using the method \textit{buildTrace}. The start point is the last state \textit{counterexampleState} which ended the verification. If the verification ends with a reachability or a deadlock, so it does not contain a loop, the trace is simply created visiting each father starting from \textit{counterexampleState} until \textit{state 0}. If instead, the verification ends with a loop, we have to eventually manipulate the data since the recorded trace using the fathers may not include a loop. If visiting each father from \textit{counterexampleState} a loop is detected, the trace is already well constructed. If instead, it does not contain a loop, a loop is searched using a deep first search starting from the loop point (the state with the same hash value of \textit{counterexampleState}). Then, the trace visiting each father starting from the loop point is appended to the previously detected cycle.
+\\\\
+In the class \textit{AvatarModelChecker} the data structures are allocated in the method \textit{initCounterexample}. The method \textit{resetCounterexample} must be used before starting a new verification to clear the data structures and to prepare the corresponding variables. Finally, the method \textit{generateCounterexample} is used to generate the traces after a verification run if a counterexample has been detected.
\end{document}
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index 5f192339466d4a728f4123e8b746b0da66e71660..b9773bf0fa8281cf7eadfb1effe195b71d4aa6fd 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -760,6 +760,17 @@ public class AvatarExpressionSolver {
}
}
+ public void setBlockIndex(AvatarSpecification spec) {
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_NO) {
+ leaf.setBlockIndex(spec);
+ }
+ } else {
+ left.setBlockIndex(spec);
+ right.setBlockIndex(spec);
+ }
+ }
+
public static boolean containsElementAttribute(AvatarElement ae) {
if (attributesMap != null) {
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 44b5770b6cce5659b93ede234bed61997af1e2d1..b7ea5c898ba8aeefc52c567123bc9f72d55b36ef 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -452,6 +452,7 @@ public class AvatarSpecification extends AvatarElement {
block.setAttributeOptRatio(attributeOptRatio);
}
}
+
//
// private void renameTimers() {
// // Check whether timers have the same name in different blocks
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index 55b610d6e49fe13db9305fdcbcd1855fc30dccae..8e2503ca024c94e7554c2618354ced581fdedfd0 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -43,6 +43,7 @@ import myutil.TraceManager;
import java.util.*;
+
/**
* Class AvatarStateMachine
* State machine, with composite states
@@ -1866,5 +1867,55 @@ public class AvatarStateMachine extends AvatarElement {
return invalids;
}
+
+
+ public List<ArrayList<AvatarTransition>> checkStaticInternalLoops() {
+ if (allStates == null) {
+ return null;
+ }
+
+ List<ArrayList<AvatarTransition>> loops = new ArrayList<ArrayList<AvatarTransition>>();
+ List<AvatarTransition> trace = new ArrayList<AvatarTransition>();
+ Set<AvatarStateMachineElement> visited= new HashSet<AvatarStateMachineElement>();
+
+ for (AvatarStateElement state : allStates) {
+ checkStaticInternalLoopsRec(state, state, trace, visited, loops, 0);
+ visited.add(state); //avoid cycles permutations
+ }
+ return loops;
+ }
+
+
+ public void checkStaticInternalLoopsRec(AvatarStateMachineElement node, AvatarStateMachineElement arrival, List<AvatarTransition> trace, Set<AvatarStateMachineElement> visited, List<ArrayList<AvatarTransition>> loops, int depth) {
+ if (visited.contains(node)) {
+ if (node == arrival) {
+ //valid loop, copy trace to loops
+ loops.add(new ArrayList<AvatarTransition>(trace));
+ return;
+ } else {
+ //not valid loop
+ return;
+ }
+ } else if (node.nexts == null){
+ return;
+ }
+
+ visited.add(node);
+ for (AvatarStateMachineElement next : node.nexts) {
+ if (next instanceof AvatarTransition) {
+ AvatarTransition at = (AvatarTransition) next;
+ //the state machine should alternate states and transitions
+ if (!(at.getNext(0) instanceof AvatarActionOnSignal)) {
+ //Choose internal action paths
+ trace.add(depth, at);
+ checkStaticInternalLoopsRec(at.getNext(0), arrival, trace, visited, loops, depth + 1);
+ trace.remove(depth);
+ }
+ }
+ }
+ visited.remove(node);
+
+ return;
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index f34898efe4aed9c0853b9f6aeb9276eae78302ff..cf64aa791ce0e84d63f15a9125a6dd4b45d129df 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -107,11 +107,19 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private ArrayList<SafetyProperty> livenesses;
private ArrayList<SafetyProperty> safeties;
private SafetyProperty safety;
+ private boolean leadsToBound;
+ private long leadsToBoundSize;
+ private boolean exitOnBound;
// Re-Initialization
private boolean studyReinit;
private SpecificationReinit initState;
+ // Internal-action loop
+ private boolean studyActionLoop;
+ private int partialHash;
+ private ArrayList<SpecificationActionLoop> actionLoops;
+
//Debug counterexample
private boolean counterexample;
private boolean counterTraceText;
@@ -155,6 +163,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
freeIntermediateStateCoding = true;
verboseInfo = true;
compressionFactor = 1;
+ partialHash = -1;
+ leadsToBound = false;
+ leadsToBoundSize = 1;
}
public AvatarSpecification getInitialSpec() {
@@ -376,6 +387,29 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return false;
}
+ public void setInternalActionLoopAnalysis(boolean studyActionLoop) {
+ this.studyActionLoop = studyActionLoop;
+ }
+
+
+ public ArrayList<SpecificationActionLoop> getInternalActionLoops() {
+ if (studyActionLoop) {
+ return actionLoops;
+ }
+ return null;
+ }
+
+ public boolean getInternalActionLoopsResult() {
+ if (studyActionLoop && actionLoops != null) {
+ for (SpecificationActionLoop sal : actionLoops) {
+ if (sal.getResult()) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
public void setCounterExampleTrace(boolean counterTraceText, boolean counterTraceAUT) {
this.counterexample = counterTraceText || counterTraceAUT;
this.counterTraceText = counterTraceText;
@@ -424,7 +458,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
public boolean startModelCheckingProperties() {
- boolean studyS, studyL, studyR, studyRI, genRG, genTrace;
+ boolean studyS, studyL, studyR, studyRI, studyAL, genRG, genTrace;
boolean emptyTr, ignoreConcurrence;
long deadlocks = 0;
@@ -449,6 +483,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyL = studyLiveness;
studyS = studySafety;
studyRI = studyReinit;
+ studyAL = studyActionLoop;
genRG = computeRG;
genTrace = counterexample;
verboseInfo = false;
@@ -460,6 +495,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyLiveness = false;
studyReachability = false;
studyReinit = false;
+ studyActionLoop = false;
counterexample = false;
@@ -485,46 +521,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = true;
counterexample = genTrace;
for (SafetyProperty sp : safeties) {
- safety = sp;
- ignoreConcurrenceBetweenInternalActions = true;
- if (safety.safetyType == SafetyProperty.LEADS_TO) {
- // prepare to save second pass states
- safetyLeadStates = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>());
- ignoreEmptyTransitions = false;
- ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
- }
- resetCounterexample();
- startModelChecking(nbOfThreads);
- generateCounterexample();
- if (safety.safetyType == SafetyProperty.LEADS_TO) {
- // second pass
- safety.initLead();
- ignoreEmptyTransitions = emptyTr;
- ignoreConcurrenceBetweenInternalActions = true;
- Iterator<Map.Entry<Integer,SpecificationState>> iter = safetyLeadStates.entrySet().iterator();
- while (iter.hasNext()) {
- SpecificationState state = iter.next().getValue();
- deadlocks += nbOfDeadlocks;
- resetModelChecking();
- resetCounterexample();
- startModelChecking(state, nbOfThreads);
- if (safety.result == false) {
- generateCounterexample();
- break;
- } else {
- //free memory
- iter.remove();
- }
- }
- System.out.println("Dimensions of lead states to elaborate: " + safetyLeadStates.size());
- safetyLeadStates = null;
- }
- if (!stoppedBeforeEnd) {
- safety.setComputed();
- }
- deadlocks += nbOfDeadlocks;
- ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
- resetModelChecking();
+ deadlocks += executeSafetyRun(sp, ignoreConcurrence, emptyTr, -1);
}
studySafety = false;
counterexample = false;
@@ -538,6 +535,34 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyReinit = false;
}
+ if (studyAL) {
+ studyActionLoop = true;
+ studySafety = true;
+ ignoreConcurrenceBetweenInternalActions = true;
+ counterexample = genTrace;
+ actionLoops = new ArrayList<SpecificationActionLoop>();
+ List<ArrayList<AvatarTransition>> internalLoops;
+ int i = 0;
+ for(AvatarBlock block : spec.getListOfBlocks()) {
+ internalLoops = block.getStateMachine().checkStaticInternalLoops();
+ if (internalLoops != null && internalLoops.isEmpty() == false) {
+ SpecificationActionLoop sap = new SpecificationActionLoop(internalLoops);
+ sap.initLeadsTo(spec);
+ if(!sap.hasError()) {
+ actionLoops.add(sap);
+ executeSafetyRun(sap.getPropertyLeadsTo(), ignoreConcurrence, false, i);
+ sap.setResultLeadsTo();
+ }
+ }
+ i++;
+ }
+ ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ counterexample = false;
+ ignoreEmptyTransitions = emptyTr;
+ studySafety = false;
+ studyActionLoop = false;
+ }
+
if (checkNoDeadlocks) {
//If a complete study with reachability graph generation has been executed,
//there is no need to study deadlocks again
@@ -581,6 +606,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = studyS;
studyReachability = studyR;
studyReinit = studyRI;
+ studyActionLoop = studyAL;
TraceManager.addDev("Model checking done");
return true;
@@ -598,10 +624,107 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
startModelChecking(nbOfThreads);
TraceManager.addDev("Model checking done");
}
+
public boolean hasBeenStoppedBeforeCompletion() {
return stoppedBeforeEnd;
}
+
+
+ private int executeSafetyRun(SafetyProperty sp, boolean ignoreConcurrence, boolean emptyTr, int partialHashing) {
+ int deadlocks = 0;
+ safety = sp;
+ ignoreConcurrenceBetweenInternalActions = true;
+ if (safety.safetyType == SafetyProperty.LEADS_TO) {
+ // prepare to save second pass states
+ safetyLeadStates = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>());
+ ignoreEmptyTransitions = false;
+ ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ partialHash = partialHashing;
+ Map<Integer, SpecificationState> statesSave = null;
+ Map<Long, SpecificationState> statesByIDSave = null;
+ List<SpecificationState> pendingStatesSave = null;
+ long stateIDSave = 0;
+ boolean loop = true;
+ boolean trace = counterexample;
+
+ leadsToBound = true;
+ leadsToBoundSize = 1;
+ exitOnBound = false;
+ counterexample = false;
+
+ startModelChecking(nbOfThreads);
+
+ //multiple pass model-checking: stop and resume states exploration to prove liveness properties
+ while (loop) {
+ if (exitOnBound) {
+ statesSave = states;
+ statesByIDSave = statesByID;
+ pendingStatesSave = pendingStates;
+ stateIDSave = stateID;
+ loop = true;
+ } else {
+ loop = false;
+ }
+
+ // second pass
+ leadsToBound = false;
+ safety.initLead();
+ ignoreEmptyTransitions = emptyTr;
+ ignoreConcurrenceBetweenInternalActions = true;
+ counterexample = trace;
+ Iterator<Map.Entry<Integer,SpecificationState>> iter = safetyLeadStates.entrySet().iterator();
+ while (iter.hasNext()) {
+ SpecificationState state = iter.next().getValue();
+ deadlocks += nbOfDeadlocks;
+ resetModelChecking();
+ resetCounterexample();
+ startModelChecking(state, nbOfThreads);
+ if (safety.result == false) {
+ generateCounterexample();
+ loop = false;
+ break;
+ } else {
+ //free memory
+ iter.remove();
+ }
+ }
+
+ if (loop) {
+ resetModelChecking();
+ safety.restoreLead();
+ states = statesSave;
+ statesByID = statesByIDSave;
+ pendingStates = pendingStatesSave;
+ stateID = stateIDSave;
+ leadsToBound = true;
+ leadsToBoundSize = leadsToBoundSize << 4;
+ exitOnBound = false;
+ counterexample = false;
+ resumeModelChecking(nbOfThreads);
+ }
+ }
+
+ statesSave = null;
+ statesByIDSave = null;
+ pendingStatesSave = null;
+
+// System.out.println("Dimensions of lead states to elaborate: " + safetyLeadStates.size());
+ safetyLeadStates = null;
+ partialHash = -1;
+ } else {
+ resetCounterexample();
+ startModelChecking(nbOfThreads);
+ generateCounterexample();
+ }
+ if (!stoppedBeforeEnd) {
+ safety.setComputed();
+ }
+ deadlocks += nbOfDeadlocks;
+ ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ resetModelChecking();
+ return deadlocks;
+ }
public void startModelChecking(int _nbOfThreads) {
@@ -738,6 +861,22 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// All done
}
+
+
+ public void resumeModelChecking(int _nbOfThreads) {
+ nbOfThreads = _nbOfThreads;
+
+ // Check data stuctures states, statesByID, and pendingStates are initialized before calling this method
+ // Check stateID contains the right value
+
+ // Check stop conditions
+ if (mustStop() || pendingStates.size() == 0) {
+ return;
+ }
+
+ nbOfCurrentComputations = 0;
+ computeAllStates();
+ }
public void stopModelChecking() {
@@ -773,11 +912,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
spec.sortAttributes();
spec.setAttributeOptRatio(compressionFactor);
spec.generateAllExpressionSolvers();
+
prepareTransitions();
prepareBlocks();
-
nbOfThreads = Runtime.getRuntime().availableProcessors();
TraceManager.addDev("Starting the model checking with " + nbOfThreads + " threads");
TraceManager.addDev("Ignore internal state:" + ignoreInternalStates);
@@ -892,14 +1031,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
emptyPendingStates();
return;
}
+
+ if (leadsToBound && safetyLeadStates.size() >= leadsToBoundSize) {
+ exitOnBound = true;
+ return;
+ }
// Pickup a state
s = pickupState();
- if ((stoppedBeforeEnd) || (stoppedConditionReached)) {
- return;
- }
-
if (s == null) {
// Terminate
go = false;
@@ -962,7 +1102,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private void resetCounterexample() {
if (counterexample) {
counterTrace.reset();
- traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
verboseInfo = true;
}
}
@@ -972,7 +1112,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (counterexample && counterTrace.hasCounterexample()) {
counterTrace.buildTrace(states, traceStates);
if (counterTraceText) {
- if (studySafety) {
+ if (studyActionLoop) {
+ counterTraceReport.append("Trace for NO internal action loops\n");
+ counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
+ } else if (studySafety) {
counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
} else if (deadlockStop) {
@@ -981,7 +1124,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
if (counterTraceAUT) {
- if (studySafety) {
+ if (studyActionLoop) {
+ counterTrace.generateTraceAUT("No internal action loops? Block " + spec.getListOfBlocks().get(partialHash).getName(), states);
+ } else if (studySafety) {
counterTrace.generateTraceAUT(safety.getRawProperty(), states);
} else if (deadlockStop) {
counterTrace.generateTraceAUT("No Deadlocks?", states);
@@ -2100,7 +2245,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (!ignoreConcurrenceBetweenInternalActions) {
state = reduceCombinatorialExplosionProperty(state);
}
- safetyLeadStates.put(state.getHash(state.getBlockValues()), state);
+ if (partialHash == -1) {
+ safetyLeadStates.put(state.getHash(state.getBlockValues()), state);
+ } else {
+ safetyLeadStates.put(state.getPartialHash(partialHash), state);
+ }
newState.property = false;
}
addToPending = 1;
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
index 260d42048594ff00b842f897c63aeb2562726aa5..b7e719384a81ad5ccaed605414e9dbb382acc8e7 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
@@ -4,6 +4,8 @@ public class CounterexampleQueryReport {
private String name;
private String query;
private String report;
+ private int nbOfStates;
+ private int nbOfTransitions;
public CounterexampleQueryReport(String name) {
this.name = name;
@@ -36,4 +38,21 @@ public class CounterexampleQueryReport {
this.report = report;
}
+ public int getNbOfStates() {
+ return nbOfStates;
+ }
+
+ public void setNbOfStates(int nbOfStates) {
+ this.nbOfStates = nbOfStates;
+ }
+
+ public int getNbOfTransitions() {
+ return nbOfTransitions;
+ }
+
+ public void setNbOfTransitions(int nbOfTransitions) {
+ this.nbOfTransitions = nbOfTransitions;
+ }
+
+
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index d6f104efc154e3c02a3378c4e04e7889c90e1f8d..18843e240089cb877456b209912bef8b97840ed7 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -266,6 +266,8 @@ public class CounterexampleTrace {
s.insert(0 ,"des(0," + (trace.size() - 1) + "," + statesID.size() + ")\n");
CounterexampleQueryReport cr = new CounterexampleQueryReport(null, query, s.toString());
+ cr.setNbOfStates(statesID.size());
+ cr.setNbOfTransitions(trace.size() - 1);
autTraces.add(cr);
}
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 4f39eff0791002e37370ef2ef27c8ef52a5a3751..967836ba91b5474764d3994d16435b8dec549b1e 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -43,10 +43,10 @@ import avatartranslator.*;
/**
* Class SafetyProperty
- * Coding of a safety property
+ * Coding of a safety or liveness property
* Creation: 22/11/2017
- * @version 1.0 22/11/2017
- * @author Ludovic APVRILLE
+ * @version 1.0 24/08/2020
+ * @author Ludovic APVRILLE, Alessandro TEMPIA CALVINO
*/
public class SafetyProperty {
@@ -77,10 +77,11 @@ public class SafetyProperty {
public int propertyType;
public int leadType;
public boolean result;
-
+ public boolean expectedResult;
public SafetyProperty(String property) {
rawProperty = property;
+ expectedResult = true;
phase = SpecificationPropertyPhase.NOTCOMPUTED;
/* to manually analyze after the AvatarSpecification is ready
for model-checking in order to build correct expression solvers */
@@ -94,6 +95,7 @@ public class SafetyProperty {
propertyType = BLOCK_STATE;
safetyType = _safetyType;
result = true;
+ expectedResult = true;
phase = SpecificationPropertyPhase.NOTCOMPUTED;
rawProperty = "Element " + state.getExtendedName() + " of block " + block.getName();
this.state = state;
@@ -103,27 +105,10 @@ public class SafetyProperty {
String tmpP = rawProperty.trim();
String p;
- errorOnProperty = NO_ERROR;
-
- if (tmpP.startsWith("A[]")) {
- safetyType = ALLTRACES_ALLSTATES;
- result = true;
- } else if (tmpP.startsWith("A<>")) {
- safetyType = ALLTRACES_ONESTATE;
- result = true;
- } else if (tmpP.startsWith("E[]")) {
- safetyType = ONETRACE_ALLSTATES;
- result = false;
- } else if (tmpP.startsWith("E<>")) {
- safetyType = ONETRACE_ONESTATE;
- result = false;
- } else if (tmpP.contains("-->")){
- safetyType = LEADS_TO;
- result = true;
- } else {
- errorOnProperty = BAD_SAFETY_TYPE;
- result = false;
- return false;
+ tmpP = checkExpectedResult(tmpP);
+
+ if (!initType(tmpP)) {
+ return false;
}
if (safetyType != LEADS_TO) {
@@ -138,10 +123,54 @@ public class SafetyProperty {
return (errorOnProperty == NO_ERROR);
}
+ //for local variables inside a block
+ public boolean analyzeProperty(AvatarBlock block, AvatarSpecification _spec) {
+ String tmpP = rawProperty.trim();
+ String p;
+
+ tmpP = checkExpectedResult(tmpP);
+
+ if (!initType(tmpP)) {
+ return false;
+ }
+
+ if (safetyType != LEADS_TO) {
+ p = tmpP.substring(3, tmpP.length()).trim();
+ initSafetyTrace(block, _spec, p);
+ } else {
+ p = tmpP;
+ initSafetyLeads(block, _spec, p);
+ }
+
+
+ return (errorOnProperty == NO_ERROR);
+ }
+
+
public void initLead() {
+ AvatarExpressionSolver tmp;
+ int type;
+ tmp = safetySolver;
safetySolver = safetySolverLead;
+ safetySolverLead = tmp;
safetyType = ALLTRACES_ONESTATE;
+ type = propertyType;
+ propertyType = leadType;
+ leadType = type;
+ result = true;
+ }
+
+ public void restoreLead() {
+ //to be used only after initLead()
+ AvatarExpressionSolver tmp;
+ int type;
+ tmp = safetySolver;
+ safetySolver = safetySolverLead;
+ safetySolverLead = tmp;
+ safetyType = LEADS_TO;
+ type = propertyType;
propertyType = leadType;
+ leadType = type;
result = true;
}
@@ -182,13 +211,14 @@ public class SafetyProperty {
public void setComputed() {
- if (result) {
+ if (result == expectedResult) {
phase = SpecificationPropertyPhase.SATISFIED;
} else {
phase = SpecificationPropertyPhase.NONSATISFIED;
}
}
+
public AvatarStateMachineElement getState() {
return state;
}
@@ -238,6 +268,44 @@ public class SafetyProperty {
return name;
}
+ private String checkExpectedResult(String tmpP) {
+ if (tmpP.startsWith("T ") || tmpP.startsWith("t ")) {
+ expectedResult = true;
+ return tmpP.substring(2).trim();
+ } else if (tmpP.startsWith("F ") || tmpP.startsWith("f ")) {
+ expectedResult = false;
+ return tmpP.substring(2).trim();
+ }
+
+ return tmpP;
+ }
+
+ private boolean initType(String tmpP) {
+ errorOnProperty = NO_ERROR;
+
+ if (tmpP.startsWith("A[]")) {
+ safetyType = ALLTRACES_ALLSTATES;
+ result = true;
+ } else if (tmpP.startsWith("A<>")) {
+ safetyType = ALLTRACES_ONESTATE;
+ result = true;
+ } else if (tmpP.startsWith("E[]")) {
+ safetyType = ONETRACE_ALLSTATES;
+ result = false;
+ } else if (tmpP.startsWith("E<>")) {
+ safetyType = ONETRACE_ONESTATE;
+ result = false;
+ } else if (tmpP.contains("-->")){
+ safetyType = LEADS_TO;
+ result = true;
+ } else {
+ errorOnProperty = BAD_SAFETY_TYPE;
+ result = false;
+ return false;
+ }
+ return true;
+ }
+
private boolean initSafetyTrace(AvatarSpecification _spec, String p) {
safetySolver = new AvatarExpressionSolver(p);
@@ -256,6 +324,25 @@ public class SafetyProperty {
return exprRet;
}
+ private boolean initSafetyTrace(AvatarBlock block, AvatarSpecification _spec, String p) {
+ safetySolver = new AvatarExpressionSolver(p);
+ boolean exprRet = safetySolver.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ }
+
+ safetySolver.setBlockIndex(_spec);
+
+ if (safetySolver.hasState()) {
+ propertyType = BLOCK_STATE;
+ } else {
+ propertyType = BOOL_EXPR;
+ }
+
+ return exprRet;
+ }
+
private boolean initSafetyLeads(AvatarSpecification _spec, String p) {
String[] pFields;
@@ -301,5 +388,54 @@ public class SafetyProperty {
return true;
}
+
+ private boolean initSafetyLeads(AvatarBlock block, AvatarSpecification _spec, String p) {
+ String[] pFields;
+ String pp, pq;
+ boolean exprRet;
+
+ pFields = p.split("-->");
+ if (pFields.length != 2) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ pp = pFields[0].trim();
+ pq = pFields[1].trim();
+
+ safetySolver = new AvatarExpressionSolver(pp);
+ exprRet = safetySolver.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ safetySolver.setBlockIndex(_spec);
+
+ safetySolverLead = new AvatarExpressionSolver(pq);
+ exprRet = safetySolverLead.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ safetySolverLead.setBlockIndex(_spec);
+
+ if (safetySolver.hasState()) {
+ propertyType = BLOCK_STATE;
+ } else {
+ propertyType = BOOL_EXPR;
+ }
+
+ if (safetySolverLead.hasState()) {
+ leadType = BLOCK_STATE;
+ } else {
+ leadType = BOOL_EXPR;
+ }
+
+ return true;
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
new file mode 100644
index 0000000000000000000000000000000000000000..d28445494f7d798bee04a54b52d0925ad22a68cf
--- /dev/null
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
@@ -0,0 +1,303 @@
+package avatartranslator.modelchecker;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import avatartranslator.AvatarBlock;
+import avatartranslator.AvatarSpecification;
+import avatartranslator.AvatarStateMachineElement;
+import avatartranslator.AvatarTransition;
+
+public class SpecificationActionLoop {
+ private List<ArrayList<AvatarTransition>> internalLoops;
+ private SafetyProperty [] reachabilities;
+ private SafetyProperty [] properties;
+ private AvatarStateMachineElement [] states;
+ private int [] cover; //0: non reachable; 1: reachable; 2: reachable with exit
+ private boolean result;
+ private boolean error;
+ private int pointer;
+
+
+ public SpecificationActionLoop(List<ArrayList<AvatarTransition>> paths) {
+ //this.path = path;
+ this.error = false;
+ pointer = 0;
+ internalLoops = paths;
+ }
+
+
+ public void init(AvatarSpecification spec) {
+ Map<AvatarStateMachineElement, Set<AvatarTransition>> map = new HashMap<>();
+
+ removeForLoops();
+
+ if (internalLoops.size() == 0) {
+ error = true;
+ return;
+ }
+
+ for (List<AvatarTransition> list : internalLoops) {
+ AvatarStateMachineElement state = list.get(list.size() -1).getNext(0); //loop state
+ for (AvatarTransition at : list) {
+ if (map.containsKey(state)) {
+ map.get(state).add(at);
+ } else {
+ Set<AvatarTransition> transitions = new HashSet<>();
+ transitions.add(at);
+ map.put(state, transitions);
+ }
+ state = at.getNext(0);
+ }
+ }
+
+ reachabilities = new SafetyProperty[map.keySet().size()];
+ properties = new SafetyProperty[map.keySet().size()];
+ states = new AvatarStateMachineElement[map.keySet().size()];
+ cover = new int[internalLoops.size()];
+
+ AvatarBlock block = (AvatarBlock) internalLoops.get(0).get(0).getBlock();
+
+ int i = 0;
+ for (AvatarStateMachineElement el : map.keySet()) {
+ Set<AvatarTransition> set = map.get(el);
+
+ states[i] = el;
+
+ SafetyProperty reachability = new SafetyProperty("E<> " + el.getName());
+ reachability.analyzeProperty(block, spec);
+ error |= reachability.hasError();
+ reachabilities[i] = reachability;
+
+ boolean guarded = false;
+ StringBuilder subCondition = new StringBuilder("!(");
+ for (AvatarTransition at : set) {
+ if (at.isGuarded()) {
+ String guard = at.getGuard().toString().replaceAll("\\[", "").trim().replaceAll("\\]", "");
+ if (guarded) {
+ subCondition.append(" || " + guard);
+ } else {
+ subCondition.append(guard);
+ }
+ guarded = true;
+ }
+ }
+ subCondition.append(")");
+ if (guarded) {
+ SafetyProperty property = new SafetyProperty("E<> " + el.getName() + " && " + subCondition.toString());
+ property.analyzeProperty(block, spec);
+ error |= property.hasError();
+ properties[i] = property;
+ }
+ i++;
+ }
+ }
+
+
+ public void initLeadsTo(AvatarSpecification spec) {
+ Set<AvatarStateMachineElement> stateSet = new HashSet<>();
+
+ removeForLoops();
+
+ if (internalLoops.size() == 0) {
+ error = true;
+ return;
+ }
+
+ for (List<AvatarTransition> list : internalLoops) {
+ for (AvatarTransition at : list) {
+ stateSet.add(at.getNext(0));
+ }
+ }
+
+ properties = new SafetyProperty[1];
+
+ AvatarBlock block = (AvatarBlock) internalLoops.get(0).get(0).getBlock();
+
+ int i = 0;
+ StringBuilder formula = new StringBuilder();
+ for (AvatarStateMachineElement el : stateSet) {
+ if (i != 0) {
+ formula.append("||");
+ }
+ formula.append(el.getName());
+ i++;
+ }
+
+ SafetyProperty property = new SafetyProperty(formula.toString() + "-->!(" + formula.toString() + ")");
+ property.analyzeProperty(block, spec);
+ error |= property.hasError();
+ properties[0] = property;
+ }
+
+ public boolean hasError() {
+ return error;
+ }
+
+ public boolean hasProperty() {
+ if (pointer < properties.length && reachabilities[pointer].result) {
+ return properties[pointer] != null;
+ }
+ return false;
+ }
+
+ public SafetyProperty getReachability() {
+ if (pointer < reachabilities.length) {
+ return reachabilities[pointer];
+ }
+ return null;
+ }
+
+ public SafetyProperty getProperty() {
+ if (pointer < properties.length && reachabilities[pointer].result) {
+ return properties[pointer];
+ }
+ return null;
+ }
+
+ public SafetyProperty getPropertyLeadsTo() {
+ return properties[0];
+ }
+
+ public boolean increasePointer() {
+ if (pointer < states.length - 1) {
+ pointer++;
+ return true;
+ }
+ return false;
+ }
+
+ public boolean setCover() {
+ int i = 0;
+
+ if (reachabilities[pointer].result) {
+ AvatarStateMachineElement state = states[pointer];
+ for (List<AvatarTransition> list : internalLoops) {
+ if (cover[i] != 2) {
+ for (AvatarTransition at : list) {
+ if (at.getNext(0) == state) {
+ if (properties[pointer] != null && properties[pointer].result) {
+ cover[i] = 2;
+ } else {
+ cover[i] = 1;
+ }
+ break;
+ }
+ }
+ }
+ i++;
+ }
+ }
+
+ for (i = 0; i < internalLoops.size(); i++) {
+ if (cover[i] != 2) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public void setResult() {
+ result = false;
+ for (int i = 0; i < internalLoops.size(); i++) {
+ if (cover[i] == 1) {
+ result = true;
+ break;
+ }
+ }
+ }
+
+ public void setResultLeadsTo() {
+ result = !properties[0].result;
+ }
+
+ public boolean getResult() {
+ return result;
+ }
+
+ public String toString() {
+ StringBuilder s = new StringBuilder();
+
+ if(internalLoops == null) {
+ return "";
+ } else if (cover == null) {
+ s.append("In block " + internalLoops.get(0).get(0).getBlock().getName() + " : ");
+ boolean first = true;
+ for (List<AvatarTransition> list : internalLoops) {
+ if (!first) {
+ s.append(", or ");
+ }
+ first = false;
+ s.append(list.get(list.size() - 1).getNext(0).getName());
+ for (AvatarTransition at : list) {
+ s.append(" --> " + at.getNext(0).getName());
+ }
+ }
+ s.append(" lead to a infinite internal loop\n");
+ return s.toString();
+ }
+
+ int i = 0;
+ for (List<AvatarTransition> list : internalLoops) {
+ if (cover[i] == 1) {
+ s.append("In block " + list.get(list.size() - 1).getBlock().getName() + " : " + list.get(list.size() - 1).getNext(0).getName());
+ for (AvatarTransition at : list) {
+ s.append(" --> " + at.getNext(0).getName());
+ }
+ }
+ i++;
+ s.append("\n");
+ }
+
+ return s.toString();
+ }
+
+ private void removeForLoops() {
+ Iterator<ArrayList<AvatarTransition>> iter = internalLoops.iterator();
+ while(iter.hasNext()) {
+ List<AvatarTransition> list = iter.next();
+ if (list.size() == 1 && list.get(0).getName().startsWith("Transition2ForRandom__")) {
+ //remove random for cycle
+ iter.remove();
+ }
+ }
+ }
+
+
+// public static void findIntersectionSets(List<ArrayList<AvatarTransition>> internalLoops) {
+// if (internalLoops == null || internalLoops.size() <= 1) {
+// return;
+// }
+//
+// internalLoops.sort((x1, x2) -> {return x2.size() - x1.size();});
+//
+// Set<AvatarStateMachineElement> states = new HashSet<>();
+// Set<AvatarStateMachineElement> intersection = new HashSet<>();
+//
+// for (AvatarTransition at : internalLoops.get(0)) {
+// states.add(at.getNext(0));
+// }
+//
+// int i = 0;
+// for (List<AvatarTransition> list : internalLoops) {
+// if (i == 0) {
+// i++;
+// continue;
+// }
+// for (AvatarTransition at : list) {
+// if (states.contains(at.getNext(0))) {
+// intersection.add(at.getNext(0));
+// }
+// }
+// if (intersection.size() != 0) {
+// states = intersection;
+// intersection = new HashSet<>();
+// }
+// }
+// }
+}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 2d4533bad7ee002d79bd774dce3ac545a067cc16..05d53ec188cdbfefa5f9e86bd66139bd54276285 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -95,6 +95,10 @@ public class SpecificationState implements Comparable<SpecificationState> {
}
return hashValue;
}
+
+ public int getPartialHash(int index) {
+ return Arrays.hashCode(blocks[index].values);
+ }
public void setInit(AvatarSpecification _spec, boolean _ignoreEmptyTransitions) {
int cpt = 0;
diff --git a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
index da00c618df0abdb040c3057eb490ac5458b9ef75..af80169f451f1841432a16247fa2318d30bc6d9f 100644
--- a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
+++ b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
@@ -177,7 +177,7 @@ public class ModelCheckerValidator {
if (dStudy) {
System.out.println("Deadlock Study");
- uResult = workQuery(gtm, rshc, "A[] not deadlock", fn);
+ uResult = workQuery(gtm, rshc, "A[] not deadlock", fn, true);
if (!((uResult == 0 && amc.getNbOfDeadlocks() > 0) || (uResult == 1 && amc.getNbOfDeadlocks() == 0))) {
diff.append("No Deadlock: amc = " + (amc.getNbOfDeadlocks() == 0) + "; uppaal = " + (uResult == 1) + "\n");
equal = false;
@@ -193,7 +193,7 @@ public class ModelCheckerValidator {
index = s.indexOf('$');
if ((index != -1)) {
query = s.substring(0, index);
- uResult = workQuery(gtm, rshc, "E<> " + query, fn);
+ uResult = workQuery(gtm, rshc, "E<> " + query, fn, true);
match = false;
for (SpecificationReachability sr : reachabilities) {
if (sr.ref1 instanceof AvatarStateMachineElement) {
@@ -228,7 +228,7 @@ public class ModelCheckerValidator {
index = s.indexOf('$');
if ((index != -1)) {
query = s.substring(0, index);
- uResult = workQuery(gtm, rshc, "A<> " + query, fn);
+ uResult = workQuery(gtm, rshc, "A<> " + query, fn, true);
match = false;
for (SafetyProperty sp : livenesses) {
Object o = sp.getState().getReferenceObject();
@@ -255,8 +255,8 @@ public class ModelCheckerValidator {
if (sStudy) {
ArrayList<SafetyProperty> safeties = amc.getSafeties();
for (SafetyProperty sp : safeties) {
- query = translateCustomQuery(gtm, spec, sp.getRawProperty());
- uResult = workQuery(gtm, rshc, query, fn);
+ query = translateCustomQuery(gtm, spec, removeExpectedResult(sp.getRawProperty()));
+ uResult = workQuery(gtm, rshc, query, fn, sp.expectedResult);
if (!(uResult == 1 && sp.getPhase() == SpecificationPropertyPhase.SATISFIED ||
uResult == 0 && sp.getPhase() == SpecificationPropertyPhase.NONSATISFIED)) {
diff.append("Safety " + sp.getRawProperty() + ": amc = " + (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) + "; uppaal = " + (uResult == 1) + "\n");
@@ -285,10 +285,19 @@ public class ModelCheckerValidator {
}
+ private static String removeExpectedResult(String query) {
+ if (query.matches("^[TtFf]\\s.*")) {
+ return query.substring(2).trim();
+ } else {
+ return query;
+ }
+ }
+
+
// return: -1: error
// return: 0: property is NOt satisfied
// return: 1: property is satisfied
- private static int workQuery(GTURTLEModeling gtm, RshClient rshc, String query, String fn) throws LauncherException {
+ private static int workQuery(GTURTLEModeling gtm, RshClient rshc, String query, String fn, boolean expectedResult) throws LauncherException {
int ret;
//TraceManager.addDev("Working on query: " + query);
@@ -307,11 +316,19 @@ public class ModelCheckerValidator {
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_VERIFIED_LABELS)) {
- ret = 1;
+ if (expectedResult) {
+ ret = 1;
+ } else {
+ ret = 0;
+ }
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_NOT_VERIFIED_LABELS)) {
- ret = 0;
+ if (!expectedResult) {
+ ret = 1;
+ } else {
+ ret = 0;
+ }
} else {
ret = -1;
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index e9ba8acdc4bd3caae911b80b8f195d98ed7b04bc..4a3e12db79ad99ba45bc0ab78250b030b7a71a32 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -42,6 +42,7 @@ package cli;
import avatartranslator.AvatarSpecification;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.CounterexampleQueryReport;
+import avatartranslator.modelchecker.SpecificationActionLoop;
import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
@@ -851,12 +852,14 @@ public class Action extends Command {
+ "-la\tliveness of all states\n"
+ "-s\tsafety pragmas verification\n"
+ "-q \"QUERY\"\tquery a safety pragma\n"
- + "-d\tno deadlocks verification\n"
+ + "-d\tno deadlocks check\n"
+ + "-i\ttest model reinitialization\n"
+ + "-a\tno internal actions loops check\n"
+ "-n NUM\tmaximum states created (Only for a non verification study)\n"
+ "-t NUM\tmaximum time (ms) (Only for a non verification study)\n"
+ "-c\tconsider full concurrency between actions\n"
- + "-v FILE\tsave counterexample traces for pragmas in FILE"
- + "-va FILE\tsave counterexample traces and AUT graph for pragmas in FILE";
+ + "-vt FILE\tsave verification traces in FILE"
+ + "-va FILE\tsave verification traces as AUT graph in FILE";
}
public String getExample() {
@@ -878,6 +881,7 @@ public class Action extends Command {
//String graphPath = commands[commands.length - 1];
String graphPath = "";
String counterPath = "";
+ String counterPathAUT = "";
AvatarSpecification avspec = interpreter.mgui.gtm.getAvatarSpecification();
if(avspec == null) {
@@ -896,6 +900,8 @@ public class Action extends Command {
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
boolean noDeadlocks = false;
+ boolean reinit = false;
+ boolean actionLoop = false;
for (int i = 0; i < commands.length; i++) {
//specification
switch (commands[i]) {
@@ -961,10 +967,20 @@ public class Action extends Command {
safetyAnalysis = true;
break;
case "-d":
- //safety
+ //deadlock
amc.setCheckNoDeadlocks(true);
noDeadlocks = true;
break;
+ case "-i":
+ //reinitialization
+ amc.setReinitAnalysis(true);
+ reinit = true;
+ break;
+ case "-a":
+ //internal action loops
+ amc.setInternalActionLoopAnalysis(true);
+ actionLoop = true;
+ break;
case "-n":
//state limit followed by a number
long states;
@@ -994,7 +1010,6 @@ public class Action extends Command {
case "-v":
if (i != commands.length - 1) {
counterPath = commands[++i];
- amc.setCounterExampleTrace(true, false);
counterTraces = true;
} else {
return Interpreter.BAD;
@@ -1002,9 +1017,7 @@ public class Action extends Command {
break;
case "-va":
if (i != commands.length - 1) {
- counterPath = commands[++i];
- amc.setCounterExampleTrace(true, true);
- counterTraces = true;
+ counterPathAUT = commands[++i];
counterTracesAUT = true;
} else {
return Interpreter.BAD;
@@ -1015,6 +1028,8 @@ public class Action extends Command {
}
}
TraceManager.addDev("Starting model checking");
+ amc.setCounterExampleTrace(counterTraces, counterTracesAUT);
+
if (livenessAnalysis || safetyAnalysis || noDeadlocks) {
amc.startModelCheckingProperties();
} else {
@@ -1026,6 +1041,21 @@ public class Action extends Command {
if (noDeadlocks) {
interpreter.print("No Deadlocks:\n" + amc.deadlockToString());
}
+ if (reinit) {
+ interpreter.print("Reinitialization?:\n" + amc.reinitToString());
+ }
+ if (actionLoop) {
+ boolean result = amc.getInternalActionLoopsResult();
+ interpreter.print("No internal action loops?:\n" + result);
+ if (!result) {
+ ArrayList<SpecificationActionLoop> al = amc.getInternalActionLoops();
+ for (SpecificationActionLoop sal : al) {
+ if (sal.getResult()) {
+ interpreter.print(sal.toString());
+ }
+ }
+ }
+ }
if (reachabilityAnalysis) {
interpreter.print("Reachability Analysis:\n" + amc.reachabilityToStringGeneric());
}
@@ -1059,6 +1089,11 @@ public class Action extends Command {
}
if (counterTracesAUT) {
+ if (counterPathAUT.indexOf("$") != -1) {
+ file = Conversion.replaceAllChar(counterPathAUT, '$', dateAndTime);
+ } else {
+ file = counterPathAUT;
+ }
List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
if (autTraces != null) {
int i = 0;
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 2f60b5f563f32622f9b7d09a1696618144bd8a91..d28497695c91dd195896b5698cbd853753230713 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -423,6 +423,16 @@ public class AvatarDesignPanelTranslator {
//Todo: check types
//Todo: handle complex types
_pragma = _pragma.trim();
+
+ if (_pragma.compareTo("") == 0) {
+ // empty pragma
+ return false;
+ }
+
+ //remove expected result letter from the start if present
+ if (_pragma.matches("^[TtFf]\\s.*")) {
+ _pragma = _pragma.substring(2).trim();
+ }
if (_pragma.contains("=") && !(_pragma.contains("==") || _pragma.contains("<=") || _pragma.contains(">=") || _pragma.contains("!="))) {
//not a query
@@ -455,10 +465,10 @@ public class AvatarDesignPanelTranslator {
String state1 = _pragma.split("-->")[0];
String state2 = _pragma.split("-->")[1];
// System.out.println("checking... " + state1 + " " + state2);
- if (!state1.contains(".") || !state2.contains(".")) {
- TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
- return false;
- }
+// if (!state1.contains(".") || !state2.contains(".")) {
+// TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
+// return false;
+// }
if (!statementParser(state1, as, _pragma, tgc)) {
return false;
}
@@ -477,6 +487,10 @@ public class AvatarDesignPanelTranslator {
} else {
+ UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " cannot be parsed: wrong or missing CTL header");
+ ce.setTDiagramPanel(adp.getAvatarBDPanel());
+ ce.setTGComponent(tgc);
+ addWarning(ce);
TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
return false;
}
@@ -496,16 +510,19 @@ public class AvatarDesignPanelTranslator {
}
state = replaceOperators(state);
- if (statementParserRec(state, as, _pragma, tgc) == 1) {
+ int returnVal = statementParserRec(state, as, _pragma, tgc);
+ if (returnVal == 1) {
UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " has invalid return type");
ce.setTDiagramPanel(adp.getAvatarBDPanel());
ce.setTGComponent(tgc);
addWarning(ce);
TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
return false;
+ } else if (returnVal == -1) {
+ return false;
+ } else {
+ return true;
}
-
- return true;
//Divide into simple statements
@@ -693,6 +710,7 @@ public class AvatarDesignPanelTranslator {
}
private int statementParserRec(String state, AvatarSpecification as, String _pragma, TGComponent tgc) {
+ //returns -1 for errors, 0 for boolean result type, and 1 for int result type
boolean isNot = false;
boolean isNegated = false;
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 1592e9e3178a095b2308ee53895d5d3d482a9124..7439a8c36df0029c70a2d1bf7cb957a0e06fa776 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -44,6 +44,7 @@ import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.CounterexampleQueryReport;
import avatartranslator.modelchecker.SafetyProperty;
+import avatartranslator.modelchecker.SpecificationActionLoop;
import avatartranslator.modelchecker.SpecificationReachability;
import avatartranslator.modelchecker.SpecificationPropertyPhase;
import myutil.*;
@@ -81,6 +82,7 @@ import java.util.concurrent.TimeUnit;
public class JDialogAvatarModelChecker extends javax.swing.JFrame implements ActionListener, Runnable, MasterProcessInterface {
private final static String[] INFOS = {"Not started", "Running", "Stopped by user", "Finished"};
private final static Color[] COLORS = {Color.darkGray, Color.magenta, Color.red, Color.blue};
+ private final static String[] WORD_BITS = {"32 bits", "16 bits", "8 bits"};
public final static int REACHABILITY_ALL = 1;
@@ -105,6 +107,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean safetySelected = false;
protected static boolean checkNoDeadSelected = false;
protected static boolean checkReinitSelected = false;
+ protected static boolean checkActionLoopSelected = false;
protected static boolean limitStatesSelected = false;
protected static boolean generateCountertraceSelected = false;
protected static boolean generateCountertraceAUTSelected = false;
@@ -112,6 +115,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static String stateLimitValue;
protected static boolean limitTimeSelected = false;
protected static String timeLimitValue;
+ protected static int wordRepresentationSelected = 1;
protected MainGUI mgui;
@@ -142,6 +146,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JButton close;
protected JButton show;
protected JButton display;
+ protected JComboBox wordRepresentationBox;
//protected JRadioButton exe, exeint;
//protected ButtonGroup exegroup;
@@ -159,6 +164,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JTextField timeLimitField;
protected JCheckBox noDeadlocks;
protected JCheckBox reinit;
+ protected JCheckBox actionLoop;
protected JCheckBox safety;
protected JCheckBox countertrace;
protected JCheckBox countertraceAUT;
@@ -269,14 +275,30 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jp01.add(generateDesign, c01);
}
+ c01.gridwidth = 1;
+
ignoreEmptyTransitions = new JCheckBox("Do not display empty transitions as internal actions", ignoreEmptyTransitionsSelected);
ignoreEmptyTransitions.addActionListener(this);
jp01.add(ignoreEmptyTransitions, c01);
+
+ c01.anchor = GridBagConstraints.EAST;
+ c01.fill = GridBagConstraints.NONE;
+ jp01.add(new JLabel("Word size: "), c01);
+
+ c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c01.anchor = GridBagConstraints.WEST;
+ c01.fill = GridBagConstraints.HORIZONTAL;
+ wordRepresentationBox = new JComboBox(WORD_BITS);
+ wordRepresentationBox.setSelectedIndex(wordRepresentationSelected);
+ wordRepresentationBox.addActionListener(this);
+ jp01.add(wordRepresentationBox, c01);
+
+
ignoreConcurrenceBetweenInternalActions = new JCheckBox("Ignore concurrency between internal actions", ignoreConcurrenceBetweenInternalActionsSelected);
ignoreConcurrenceBetweenInternalActions.addActionListener(this);
jp01.add(ignoreConcurrenceBetweenInternalActions, c01);
- ignoreInternalStates = new JCheckBox("Ignore states between internal actions",
- ignoreInternalStatesSelected);
+
+ ignoreInternalStates = new JCheckBox("Ignore states between internal actions", ignoreInternalStatesSelected);
ignoreInternalStates.addActionListener(this);
jp01.add(ignoreInternalStates, c01);
@@ -321,10 +343,15 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Reinit
- cbasic.gridwidth = GridBagConstraints.REMAINDER;
reinit = new JCheckBox("Reinitialization?", checkReinitSelected);
reinit.addActionListener(this);
jpbasic.add(reinit, cbasic);
+
+ // Internal action loop
+ cbasic.gridwidth = GridBagConstraints.REMAINDER;
+ actionLoop = new JCheckBox("No internal action loops?", checkActionLoopSelected);
+ actionLoop.addActionListener(this);
+ jpbasic.add(actionLoop, cbasic);
// Reachability
@@ -729,12 +756,13 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
timer.scheduleAtFixedRate(mcm, 0, 500);
// Setting options
- amc.setCompressionFactor(2);
+ amc.setCompressionFactor(wordRepresentationSelected << 1);
amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
+ amc.setInternalActionLoopAnalysis(checkActionLoopSelected);
amc.setCounterExampleTrace(generateCountertraceSelected, generateCountertraceAUTSelected);
// Reachability
@@ -838,7 +866,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Starting model checking
testGo();
- if (livenessSelected == LIVENESS_NONE && safetySelected == false && checkNoDeadSelected == false) {
+ if (livenessSelected == LIVENESS_NONE && safetySelected == false && checkNoDeadSelected == false && checkActionLoopSelected == false) {
amc.startModelChecking();
} else {
amc.startModelCheckingProperties();
@@ -869,6 +897,27 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (checkReinitSelected) {
jta.append("\nReinitialization?\n" + "-> " + amc.reinitToString() + "\n");
}
+
+ if (checkActionLoopSelected) {
+ boolean result = amc.getInternalActionLoopsResult();
+ String s;
+ if (result) {
+ s = "property is satisfied";
+ } else {
+ s = "property is NOT satisfied";
+ }
+ jta.append("\nNo internal action loops?\n" + "-> " + s + "\n");
+ if (!result) {
+ ArrayList<SpecificationActionLoop> al = amc.getInternalActionLoops();
+ jta.append("Internal action loops:\n");
+ for (SpecificationActionLoop sal : al) {
+ if (sal.getResult()) {
+ jta.append(sal.toString());
+ }
+ }
+ jta.append("\n");
+ }
+ }
if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
jta.append("\nReachabilities found:\n");
@@ -934,6 +983,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
RG rg = new RG(file);
rg.data = tr.getReport();
rg.fileName = filename;
+ rg.nbOfStates = tr.getNbOfStates();
+ rg.nbOfTransitions = tr.getNbOfTransitions();
rg.name = tr.getQuery() + "_" + dateAndTime;
mgui.addRG(rg);
File f = new File(filename);
@@ -1090,6 +1141,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
ignoreInternalStatesSelected = ignoreInternalStates.isSelected();
checkNoDeadSelected = noDeadlocks.isSelected();
checkReinitSelected = reinit.isSelected();
+ checkActionLoopSelected = actionLoop.isSelected();
+ wordRepresentationSelected = wordRepresentationBox.getSelectedIndex();
if (noReachability.isSelected()) {
reachabilitySelected = REACHABILITY_NONE;
@@ -1115,9 +1168,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
- countertrace.setEnabled(safety.isSelected() || noDeadlocks.isSelected());
- countertraceAUT.setEnabled(safety.isSelected() || noDeadlocks.isSelected());
- countertraceField.setEnabled(countertrace.isSelected());
+ countertrace.setEnabled(safety.isSelected() || noDeadlocks.isSelected() || actionLoop.isSelected());
+ countertraceAUT.setEnabled(safety.isSelected() || noDeadlocks.isSelected() || actionLoop.isSelected());
+ countertraceField.setEnabled(countertrace.isSelected() || countertraceAUT.isSelected());
generateCountertraceSelected = countertrace.isSelected();
generateCountertraceAUTSelected = countertraceAUT.isSelected();
@@ -1129,7 +1182,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
switch (mode) {
case NOT_STARTED:
- if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || checkReinitSelected || graphSelected || graphSelectedDot) {
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || checkReinitSelected || checkActionLoopSelected || graphSelected || graphSelectedDot) {
start.setEnabled(true);
} else {
if (safetySelected) {
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index aee111931558b0132fb3ad5e5fc03fe5ed6f3f9b..ff6a3510318708ec6c78a4d8e3b099fb0a0d9df5 100644
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -152,6 +152,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected java.util.List<String> customQueries;
public Map<String, Integer> verifMap;
protected int status = -1;
+ private boolean expectedResult;
/*
* Creates new form
@@ -619,6 +620,9 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
rshc = new RshClient(host);
RshClient rshctmp = rshc;
+
+ expectedResult = true;
+
try {
// checking UPPAAL installation
@@ -795,7 +799,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
for (JCheckBox j : customChecks) {
if (j.isSelected()) {
jta.append(j.getText() + "\n");
- String translation = translateCustomQuery(j.getText());
+ String translation = checkExpectedResult(j.getText());
+ translation = translateCustomQuery(translation);
jta.append(translation);
status = -1;
workQuery(translation, fn, trace_id, rshc);
@@ -859,6 +864,20 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
mode = NOT_STARTED;
setButtons();
}
+
+ private String checkExpectedResult(String query) {
+ query = query.trim();
+ expectedResult = true;
+
+ if (query.startsWith("T ") || query.startsWith("t ")) {
+ return query.substring(2).trim();
+ } else if (query.startsWith("F ") || query.startsWith("f ")) {
+ expectedResult = false;
+ return query.substring(2).trim();
+ }
+
+ return query;
+ }
private String translateCustomQuery(String query) {
@@ -979,16 +998,26 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_VERIFIED_LABELS)) {
// else if (data.indexOf("Property is satisfied") >-1){
- jta.append("-> property is satisfied\n");
- status = 1;
+ if (expectedResult) {
+ jta.append("-> property is satisfied\n");
+ status = 1;
+ } else {
+ jta.append("-> property is NOT satisfied\n");
+ status = 0;
+ }
ret = 1;
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_NOT_VERIFIED_LABELS)) {
// else if (data.indexOf("Property is NOT satisfied") > -1) {
- jta.append("-> property is NOT satisfied\n");
- status = 0;
- ret = 0;
+ if (!expectedResult) {
+ jta.append("-> property is satisfied\n");
+ status = 1;
+ } else {
+ jta.append("-> property is NOT satisfied\n");
+ status = 0;
+ }
+ ret = 1;
} else {
jta.append("ERROR -> property could not be studied\n");
status = 2;
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index 7a8aab6f28c4df6b56bb2be5b0c13f590e8d3235..bd13777cc97fa61efad5fc074d726d53d9c8fdb0 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -126,12 +126,15 @@ public class AvatarExpressionTest {
assertTrue(e9.buildExpression());
AvatarExpressionSolver e10 = new AvatarExpressionSolver("true && 0 >= 1 || false");
assertTrue(e10.buildExpression());
+ AvatarExpressionSolver e11 = new AvatarExpressionSolver("8/2*(2+2)");
+ assertTrue(e11.buildExpression());
assertTrue(e1.getResult() == 1);
assertTrue(e2.getResult() == 1);
assertTrue(e3.getResult() == 0);
assertTrue(e5.getResult() == 1);
assertTrue(e9.getResult() == 1);
assertTrue(e10.getResult() == 0);
+ assertTrue(e11.getResult() == 16);
}
@Test