diff --git a/doc/avatarmodelchecker/images/conc_blocks.png b/doc/avatarmodelchecker/images/conc_blocks.png
new file mode 100644
index 0000000000000000000000000000000000000000..98c4f0d067c0d0f3017bf2a69d48031379a30d84
Binary files /dev/null and b/doc/avatarmodelchecker/images/conc_blocks.png differ
diff --git a/doc/avatarmodelchecker/images/conc_main.png b/doc/avatarmodelchecker/images/conc_main.png
new file mode 100644
index 0000000000000000000000000000000000000000..15d9be4ed4e10a6404872833962a6997dc031331
Binary files /dev/null and b/doc/avatarmodelchecker/images/conc_main.png differ
diff --git a/doc/avatarmodelchecker/images/conc_sensor.png b/doc/avatarmodelchecker/images/conc_sensor.png
new file mode 100644
index 0000000000000000000000000000000000000000..246ebc6d9a2c0da1cc01753946771ab9a27e8bf2
Binary files /dev/null and b/doc/avatarmodelchecker/images/conc_sensor.png differ
diff --git a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
index 7b91683d4b1bd0f86d5afcb790453b203b49be33..c31f168e28d27c38942deffdce57ba8822c398fe 100644
--- a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
+++ b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
@@ -20,6 +20,7 @@
\usepackage{hyperref}
\usepackage{listings}
\usepackage{color}
+\usepackage[labelfont=sf,hypcap=false,format=hang,width=0.8\columnwidth]{caption}
\definecolor{pblue}{rgb}{0.13,0.13,1}
\definecolor{pgreen}{rgb}{0,0.5,0}
@@ -131,18 +132,18 @@ Editor} & \textbf{Year}
\subsection{Executive Summary}
-This document describes how the AVATAR model checker of TTool works. This document explains the data structure used to represent the models, the algorithm for reachability graph generation, and the properties that can be verified.
+This document describes how the AVATAR model checker of TTool works. This document is divided mainly into two parts. The first one is the user guide on how to use the model-checker. The second one explains the data structure used to represent the models, the algorithm for reachability graph generation, and the properties that can be verified.
-\newpage
+\newpage
\section{A First Example}
-This very first example explains how to verify reachability, liveness and safety properties using the AVATAR model-checker on a design model.
+This very first example explains how to verify reachability, liveness, and safety properties using the AVATAR model-checker on a design model.
\subsection{Getting the example}
Be sure to get the latest version of TTool including the remote loading of models (June 2020 and after). Do: File, Open from TTool repository, and select "PressureController.xml". Then, open the design panel to view the AVATAR design model.
\subsection{Understanding the model}
-The Pressure Controller is build upon a set of blocks representing the system itself, and two blocks representing the environment (the pressure sensor, and the alarm actuator), see Figure \ref{fig:pressurecontroller}.
+The Pressure Controller is built upon a set of blocks representing the system itself, and two blocks representing the environment (the pressure sensor, and the alarm actuator), see Figure \ref{fig:pressurecontroller}.
\begin{figure}[h]
\centering
@@ -152,7 +153,7 @@ The Pressure Controller is build upon a set of blocks representing the system it
\end{figure}
\subsubsection{PressureSensor}
-The pressure sensor (see Figure \ref{fig:pressuresensor}) monitors the pressure with a period of 20 units of time. In the first branch, "IsInCode" method that is \textbf{not} executed when the model is considered for functional simulation or formal verification. Indeed, in our case, the "branch" boolean is set to false by default, so the random command is executed (and not the readingPressure() method). The random value, between 18 and 21, is sent every period of time to the main controller.
+The pressure sensor (see Figure \ref{fig:pressuresensor}) monitors the pressure with a period of 20 units of time. In the first branch, "IsInCode" method is \textbf{not} executed when the model is considered for functional simulation or formal verification. Indeed, in our case, the "branch" boolean is set to false by default, so the random command is executed (and not the readingPressure() method). The random value, between 18 and 21, is sent every period of time to the main controller.
\begin{figure}[h!]
\centering
@@ -172,7 +173,7 @@ The main controller (see Figure \ref{fig:maincontroller}) receives the pressure
\end{figure}
\subsubsection{AlarmManager}
-The alarm manager (see Figure \ref{fig:alarmmanager}) activates an alarm when the controller senses a high pressure. The alarm is deactivated after "alarmDuration", controlled by a timer, if no other high pressure signals are sensed.
+The alarm manager (see Figure \ref{fig:alarmmanager}) activates an alarm when the controller senses a high pressure. The alarm is deactivated after "alarmDuration", controlled by a timer, if no other high pressure signals are sensed in the meanwhile.
\begin{figure}[h!]
\centering
@@ -186,28 +187,28 @@ The alarm actuator may receive on and off signals activating and deactivating th
\subsection{Reachability and liveness}
-For specific states, we can activate the reachability and liveness check going to the correspondant state machine, right clicking on a state or a signal and selecting "Check for Reachability / Liveness". For instance, let's do that on the \textit{AlarmIsOn} state in the AlarmManager state machine. After the operation, the letters R and L in grey will appear next to the state (see Figure \ref{fig:rl_grey}) to confirm that the state is selected for the reachability and liveness check. After that, we may proceed with the verification.
+To activate the reachability and liveness check for specific states, we need to go to the correspondant block state machine, right click on a state or a signal and select "Check for Reachability / Liveness". For instance, let's do that on the \textit{AlarmIsOn} state in the AlarmManager state machine. After this operation, the letters R and L in grey will appear next to the state (see Figure \ref{fig:rl_grey}) to confirm that the state is selected for the reachability and liveness check. After that, we may proceed with the verification.
\begin{figure}[h!]
\centering
\includegraphics[width=0.5\textwidth]{images/rl_grey.jpg}
\caption{State selected for reachability and liveness check}
\label{fig:rl_grey}
\end{figure}
-\\To open the model-checker window, we must first compile the model. To do that, let's click on the "syntax analysis" icon and then on "check syntax" to compile the model. Then,, we click on the "safety veification (internal tool)" icon representing a screwdriver and a wrench with the text "RC". The following window should open (see Figure \ref{fig:mcwindow}).
+\\To open the model-checker window, we must first compile the model. To do that, let's click on the "syntax analysis" icon and then on "check syntax". Then, we click on the "safety verification (internal tool)" icon representing a screwdriver and a wrench crossed with the text "RC". The following window should open (see Figure \ref{fig:mcwindow}).
\begin{figure}[h!]
\centering
\includegraphics[width=\textwidth]{images/modelcheckerwindow.jpg}
\caption{Model-checker window}
\label{fig:mcwindow}
\end{figure}
-\\To execute the reachability and liveness check on the selected state, let's select "Selected states" in both Reachability and Liveness lines. Then, we can press the start button. The text area will contain the verification report indicating if the properties are satisfied or not. Moreover, if we go back to the AlarmManager state machine, the RL text next to the state is colored with green for \textit{satisfied} and in red for \textit{not satisfied} (see Figure \ref{fig:rl_exe}).
+\\To execute the reachability and liveness check on the selected state, let's select "Selected states" in both Reachability and Liveness lines. Then, we can press the start button. The text area will contain the verification report indicating if the properties are satisfied or not. Moreover, if we go back to the AlarmManager state machine, the RL text next to the state is now colored with green for \textit{satisfied} and in red for \textit{not satisfied} (see Figure \ref{fig:rl_exe}).
\begin{figure}[h!]
\centering
\includegraphics[width=0.5\textwidth]{images/rl_exe.jpg}
\caption{Reachability and Liveness result}
\label{fig:rl_exe}
\end{figure}
-\\In this case, the reachability is satisfied as it is possible that the pressure sensor detects a temperature higher than the controller threshold. The liveness, instead, is not satisfied as it is possible that a temperature higher than the threshold is never detected.
+\\In this case, the reachability is satisfied as the pressure sensor may detect a temperature higher than the controller threshold. The liveness, instead, is not satisfied as a temperature higher than the threshold may be never detected.
\\\\
If we want to simply verify the reachability and liveness property automatically for all the states, we can select "All states" in the model-checking window.
@@ -221,7 +222,7 @@ We can find, write and modify safety properties in the block diagram tab inside
\end{figure}
\\If we do a double click on the pink box, we see the safety and liveness pragmas written as a CTL formula using UPPAAL syntax. If we press the question mark in the window, a short illustrated guide on how the queries work appears.
\\\\
-To start the CTL query verification, let's compile again and let's open the model-checker wiindow. As shown in figure \ref{fig:mcwindow}, we want to select the checkbox "Safety pragmas" and then we select the queries that we want to verify. In this case, let's execute them all. Let's press the start butto to begin the verification. The query results is shown both in the report field in the window and in the pink box in the block diagram tab (see Picture \ref{fig:sresult}).
+To start the CTL query verification, let's compile again and let's open the model-checker window. As shown in figure \ref{fig:mcwindow}, we want to select the checkbox "Safety pragmas" and then we select the queries that we want to verify. In this case, let's execute all of them. Let's press the start button to begin the verification. The query results are shown both in the report field and inside the pink box in the block diagram tab (see Picture \ref{fig:sresult}).
\begin{figure}[h!]
\centering
\includegraphics[width=0.7\textwidth]{images/safety_result.png}
@@ -230,13 +231,13 @@ To start the CTL query verification, let's compile again and let's open the mode
\end{figure}
\newpage
-\section{Verification Guide}
-In this section we will explain all the features and all the options that are present in the AVATAR model-checker. As window reference, please refer to figure \ref{fig:mcwindow}.
+\section{Verification Guide} \label{sec:vg}
+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{Do not display empty transitions as internal states}: in the reachability graph generation, states are created also for empty transitions (no action, no time, no choice). This option does not affect the verification.
- \item \textbf{Ignore concurrency between internal actions}: this option allow to ignore a full concurrency study. It is very useful to limit the state explosion of the model due to all the concurrencies among states. It is so suggested to keep it selected to have a faster verification. This option, however, it is considered only in the \textit{leadsto} study, as it is the only study that might be affected by this option, and in the reachability graph generation. \textbf{Important}: basic concurrency it is evaluated also with this optimization selected. Basic concurrency means that the concurrency is evaluated until states with multiple transitions, if statement, and signals communitation (things that are evaluated in not selected mode) are encounted. In normal usage, you should not need to deselect this option.
- \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 is not used. We suggest to keep this option selected for verification as it would not affect the result.
+ \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.
\item \textbf{Limit the number of states in RG}: it limits the reachability graph generation to a fixed number of states. It is particularly useful for big models. This option is automatically ignored when a verification study is selected.
\item \textbf{Time constraint for RG generation}: it allows to stop the reachability graph generation after a fixed number of milliseconds. It is particularly useful for big models. This option is automatically ignored when a verification study is selected.
\end{itemize}
@@ -244,12 +245,12 @@ 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{Reachability}: it checks states reachability
+ \item \textbf{Reachability}: it checks for states reachability
\item \textbf{Liveness}: it checks for states liveness
\end{itemize}
-The next section allows advanced options to be selected. It allows to execute safety and liveness pragmas written as a CTL formula. Each of them can be selected or not for the verification.
+The next section allows to execute safety and liveness pragmas written as a CTL formula. Each of them can be selected or not for the verification.
\\\\
-Then, if \textbf{Reachability Graph Generation} options is used to generate and save the reachability graph. Moreover, it can can be saved also in "dotty" format.
+Then, \textbf{Reachability Graph Generation} options is used to generate and save the reachability graph. Moreover, it can can be saved also in "dotty" format.
\subsection{CTL query syntax}
The query syntax for CTL formulas, for expressions \texttt{p} and \texttt{q}, is the following:
@@ -260,13 +261,43 @@ 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 attributes. 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 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:
\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{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.
\end{itemize}
+\subsection{Concurrency behavior} \label{sec:cb}
+In section \ref{sec:vg}, we discussed about the option \textit{Ignore concurrency between internal actions} and how it could effect the model-checker behavior. In this section, we will show with a guided example the differences between having this option on or off.
+\\\\
+In this simplified example (see Figure \ref{fig:cb}), we have two blocks: a sensor and a main block that receive the informations.
+\begin{figure}[h!]
+\centering
+\includegraphics[width=0.8\textwidth]{images/conc_blocks.png}
+\caption{Example on concurrency}
+\label{fig:cb}
+\end{figure}
+Let's consider the two blocks connected through a synchronous channel. Also with asynchronous there would not be any difference in this analysis. The two states machine are shown in figure \ref{fig:csm}.
+\begin{table}[h!]
+ \begin{center}
+ \begin{tabular}{ c c }
+ \includegraphics[scale=0.6]{images/conc_sensor.png}
+ &
+ \includegraphics[scale=0.6]{images/conc_main.png}
+ \\
+ (a)
+ &
+ (b)
+ \end{tabular}
+ \end{center}
+ \captionof{figure}{Sensor (a) and Main (b) state machines}
+ \label{fig:csm}
+\end{table}\\\\
+First, we want to prove that after Sensor.Sent, Main will eventually reach the Receive state (\textit{Sensor.Sent --> Main.Receive}). After the data is sent by the sensor and received by the main block, the is a concurrency between executing first the Sent state or the Received state. In this case, both with the option \textit{Ignore concurrency between internal actions} selected or not, the pragma result will be always false. In fact, the Received state may be reached before Sent.\\
+Different is the case for the following pragma: \textit{Sensor.Sent --> Main.Restart}. In this case, after the Received state, there are two possible choices: Elaborate and Ignore. If the option \textit{Ignore concurrency between internal actions} is selected, the single transitions have priority over the choices. This will lead to Sent being reached before Elaborate or Ignore. The pragma will be true. If the option is not selected instead, a full concurrency study is executed and the pragma will result correctly false. Note that a full concurrency study will considerably slow down the verification performance.
+\\\\
+The best way to avoid concurrency problems and to keep this option always selected is to ask concurrency aware queries. If we want to check if something happens after sending the data, the best choice would be to query \textit{Sensor.Wait --> Main.Restart}. This query does not depend by concurrency since it happens before a "synchronization" point.
\newpage
\section{AVATAR Model-Checker}
diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index bcf8ffe0352006892e0d729fbd5b6d457ca87413..d4559085174036dbddb44876cd5294f481c1fc66 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -38,6 +38,8 @@
package avatartranslator;
+import java.util.List;
+
import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState;
@@ -204,6 +206,19 @@ public class AvatarExpressionAttribute {
return value;
}
+ public int getValue(int[] attributesValues) {
+ int value;
+
+ if (isState) {
+ return 0;
+ }
+
+ //Cancel offset based on Specification Blocks
+ value = attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX];
+
+ return value;
+ }
+
public void setValue(SpecificationState ss, int value) {
int v;
@@ -239,6 +254,18 @@ public class AvatarExpressionAttribute {
}
}
+
+ public int getAttributeType() {
+ if (isState) {
+ return AvatarExpressionSolver.IMMEDIATE_BOOL;
+ } else if (block.getAttribute(accessIndex - SpecificationBlock.ATTR_INDEX).getType() == AvatarType.BOOLEAN) {
+ return AvatarExpressionSolver.IMMEDIATE_BOOL;
+ } else {
+ return AvatarExpressionSolver.IMMEDIATE_INT;
+ }
+ }
+
+
public boolean isState() {
return isState;
}
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index e73a5c237c823a4d6816b7a2cd46ed9b4b5e9ee9..bacb6d4639fefafb34f660936046a6548c70d10b 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -50,8 +50,10 @@ import avatartranslator.modelchecker.SpecificationState;
* @version 1.0 17/04/2020
*/
public class AvatarExpressionSolver {
- private static final int IMMEDIATE_NO = 0;
- private static final int IMMEDIATE_INT = 1;
+ protected static final int IMMEDIATE_NO = 0;
+ protected static final int IMMEDIATE_INT = 1;
+ protected static final int IMMEDIATE_BOOL = 2;
+
private AvatarExpressionSolver left, right;
private char operator;
@@ -59,7 +61,7 @@ public class AvatarExpressionSolver {
private boolean isLeaf; //variable
private boolean isNot;
private boolean isNegated;
- private int isImmediateValue; //0: No; 1: Boolean; 2: Int
+ private int isImmediateValue; //0: No; 1: Int; 2: Boolean;
private int intValue;
private AvatarExpressionAttribute leaf;
@@ -93,6 +95,48 @@ public class AvatarExpressionSolver {
public boolean buildExpression(AvatarSpecification spec) {
boolean returnVal;
+ returnVal = buildExpressionRec(spec);
+ if (returnVal == false) {
+ return false;
+ }
+
+ return checkIntegrity();
+ }
+
+ public boolean buildExpression(AvatarBlock block) {
+ boolean returnVal;
+
+ returnVal = buildExpressionRec(block);
+ if (returnVal == false) {
+ return false;
+ }
+
+ return checkIntegrity();
+ }
+
+ public boolean buildExpression() {
+ boolean returnVal;
+
+ returnVal = buildExpressionRec();
+ if (returnVal == false) {
+ return false;
+ }
+
+ return checkIntegrity();
+ }
+
+ public boolean builExpression(AvatarExpressionAttribute attribute) {
+ this.expression = attribute.toString();
+ isLeaf = true;
+ isImmediateValue = IMMEDIATE_NO;
+ leaf = attribute;
+ return true;
+ }
+
+
+ public boolean buildExpressionRec(AvatarSpecification spec) {
+ boolean returnVal;
+
removeUselessBrackets();
if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
@@ -103,11 +147,11 @@ public class AvatarExpressionSolver {
checkNegatedNoBrackets();
if (expression.equals("true")) {
intValue = 1;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.equals("false")) {
intValue = 0;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.matches("-?\\d+")) {
intValue = Integer.parseInt(expression);
@@ -145,13 +189,13 @@ public class AvatarExpressionSolver {
left = new AvatarExpressionSolver(leftExpression);
right = new AvatarExpressionSolver(rightExpression);
//System.out.println("Expression " + expression + " ; " + leftExpression + " ; " + rightExpression + "\n");
- returnVal = left.buildExpression(spec);
- returnVal &= right.buildExpression(spec);
+ returnVal = left.buildExpressionRec(spec);
+ returnVal &= right.buildExpressionRec(spec);
return returnVal;
}
- public boolean buildExpression(AvatarBlock block) {
+ public boolean buildExpressionRec(AvatarBlock block) {
boolean returnVal;
removeUselessBrackets();
@@ -164,11 +208,11 @@ public class AvatarExpressionSolver {
checkNegatedNoBrackets();
if (expression.equals("true")) {
intValue = 1;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.equals("false")) {
intValue = 0;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.matches("-?\\d+")) {
intValue = Integer.parseInt(expression);
@@ -206,21 +250,14 @@ public class AvatarExpressionSolver {
left = new AvatarExpressionSolver(leftExpression);
right = new AvatarExpressionSolver(rightExpression);
//System.out.println("Expression " + expression + " ; " + leftExpression + " ; " + rightExpression + "\n");
- returnVal = left.buildExpression(block);
- returnVal &= right.buildExpression(block);
+ returnVal = left.buildExpressionRec(block);
+ returnVal &= right.buildExpressionRec(block);
return returnVal;
}
- public boolean builExpression(AvatarExpressionAttribute attribute) {
- this.expression = attribute.toString();
- isLeaf = true;
- isImmediateValue = IMMEDIATE_NO;
- leaf = attribute;
- return true;
- }
- public boolean buildExpression() {
+ public boolean buildExpressionRec() {
boolean returnVal;
removeUselessBrackets();
@@ -233,11 +270,11 @@ public class AvatarExpressionSolver {
checkNegatedNoBrackets();
if (expression.equals("true")) {
intValue = 1;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.equals("false")) {
intValue = 0;
- isImmediateValue = IMMEDIATE_INT;
+ isImmediateValue = IMMEDIATE_BOOL;
returnVal = true;
} else if (expression.matches("-?\\d+")) {
intValue = Integer.parseInt(expression);
@@ -274,8 +311,8 @@ public class AvatarExpressionSolver {
left = new AvatarExpressionSolver(leftExpression);
right = new AvatarExpressionSolver(rightExpression);
//System.out.println("Expression " + expression + " ; " + leftExpression + " ; " + rightExpression + "\n");
- returnVal = left.buildExpression();
- returnVal &= right.buildExpression();
+ returnVal = left.buildExpressionRec();
+ returnVal &= right.buildExpressionRec();
return returnVal;
}
@@ -346,43 +383,55 @@ public class AvatarExpressionSolver {
for (i = 0, index = -1; i < expression.length(); i++) {
a = expression.charAt(i);
switch (a) {
- case '=':
+ case '|':
if (level == 0) {
index = i;
- priority = 2;
+ priority = 5;
+ }
+ break;
+ case '&':
+ if (level == 0 && priority < 5) {
+ index = i;
+ priority = 4;
+ }
+ break;
+ case '=':
+ if (level == 0 && priority < 4) {
+ index = i;
+ priority = 3;
}
subVar = true;
break;
case '$':
- if (level == 0) {
+ if (level == 0 && priority < 4) {
index = i;
- priority = 2;
+ priority = 3;
}
subVar = true;
break;
case '<':
- if (level == 0) {
+ if (level == 0 && priority < 3) {
index = i;
priority = 2;
}
subVar = true;
break;
case '>':
- if (level == 0) {
+ if (level == 0 && priority < 3) {
index = i;
priority = 2;
}
subVar = true;
break;
case ':':
- if (level == 0) {
+ if (level == 0 && priority < 3) {
index = i;
priority = 2;
}
subVar = true;
break;
case ';':
- if (level == 0) {
+ if (level == 0 && priority < 3) {
index = i;
priority = 2;
}
@@ -400,12 +449,6 @@ public class AvatarExpressionSolver {
priority = 1;
}
break;
- case '|':
- if (level == 0 && priority < 2) {
- index = i;
- priority = 1;
- }
- break;
case '/':
if (level == 0 && priority == 0) {
index = i;
@@ -416,11 +459,6 @@ public class AvatarExpressionSolver {
index = i;
}
break;
- case '&':
- if (level == 0 && priority == 0) {
- index = i;
- }
- break;
case '(':
level++;
subVar = true;
@@ -442,7 +480,7 @@ public class AvatarExpressionSolver {
public int getResult() {
int res;
if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_INT) {
+ if (isImmediateValue != IMMEDIATE_NO) {
res = intValue;
} else {
return 0;
@@ -462,7 +500,7 @@ public class AvatarExpressionSolver {
public int getResult(SpecificationState ss) {
int res;
if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_INT) {
+ if (isImmediateValue != IMMEDIATE_NO) {
res = intValue;
} else {
res = leaf.getValue(ss);
@@ -482,7 +520,7 @@ public class AvatarExpressionSolver {
public int getResult(SpecificationState ss, AvatarStateMachineElement asme) {
int res;
if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_INT) {
+ if (isImmediateValue != IMMEDIATE_NO) {
res = intValue;
} else {
res = leaf.getValue(ss, asme);
@@ -502,7 +540,7 @@ public class AvatarExpressionSolver {
public int getResult(SpecificationBlock sb) {
int res;
if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_INT) {
+ if (isImmediateValue != IMMEDIATE_NO) {
res = intValue;
} else {
res = leaf.getValue(sb);
@@ -519,6 +557,26 @@ public class AvatarExpressionSolver {
return res;
}
+ public int getResult(int[] attributesValues) {
+ int res;
+ if (isLeaf) {
+ if (isImmediateValue != IMMEDIATE_NO) {
+ res = intValue;
+ } else {
+ res = leaf.getValue(attributesValues);
+ }
+ } else {
+ res = getChildrenResult(left.getResult(attributesValues), right.getResult(attributesValues));
+ }
+
+ if (isNot) {
+ res = (res == 0) ? 1 : 0;
+ } else if (isNegated) {
+ res = -res;
+ }
+ return res;
+ }
+
private int getChildrenResult(int leftV, int rightV) {
int result;
@@ -573,8 +631,14 @@ public class AvatarExpressionSolver {
if (isLeaf) {
if (isImmediateValue == IMMEDIATE_NO) {
retS = leaf.toString();
- } else {
+ } else if (isImmediateValue == IMMEDIATE_INT){
retS = String.valueOf(intValue);
+ } else {
+ if (intValue == 0) {
+ retS = "false";
+ } else {
+ retS = "true";
+ }
}
if (isNegated) {
retS = "-(" + retS + ")";
@@ -646,6 +710,51 @@ public class AvatarExpressionSolver {
}
}
+ private boolean checkIntegrity() {
+ int optype, optypel, optyper;
+ boolean returnVal;
+
+ if (isLeaf) {
+ if (isNot) {
+ return getReturnType() == IMMEDIATE_BOOL;
+ } else if (isNegated) {
+ return getReturnType() == IMMEDIATE_INT;
+ } else {
+ return true;
+ }
+ }
+
+ optype = getType();
+ optypel = left.getReturnType();
+ optyper = right.getReturnType();
+
+ switch(optype) {
+ case IMMEDIATE_NO:
+ returnVal = false; //Error
+ break;
+ case IMMEDIATE_INT:
+ returnVal = (optypel == IMMEDIATE_INT && optyper == IMMEDIATE_INT) ? true : false;
+ break;
+ case IMMEDIATE_BOOL:
+ returnVal = (optypel == IMMEDIATE_BOOL && optyper == IMMEDIATE_BOOL) ? true : false;
+ break;
+ case 3:
+ returnVal = (optypel == optyper) ? true : false;
+ break;
+ default:
+ returnVal = false;
+ }
+
+ if (returnVal == false) {
+ return false;
+ }
+
+ returnVal = left.checkIntegrity();
+ returnVal &= right.checkIntegrity();
+
+ return returnVal;
+ }
+
private void removeUselessBrackets() {
while (expression.startsWith("(") && expression.endsWith(")")) {
if (getClosingBracket(1) == expression.length() - 1) {
@@ -673,5 +782,79 @@ public class AvatarExpressionSolver {
}
return -1;
}
+
+ private int getType() {
+ int optype;
+
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_NO) {
+ return leaf.getAttributeType();
+ } else {
+ return isImmediateValue;
+ }
+ }
+
+ switch (operator) {
+ case '=':
+ case '$':
+ optype = 3; //BOTH sides must have the same type
+ break;
+ case '<':
+ case '>':
+ case ':':
+ case ';':
+ case '-':
+ case '+':
+ case '/':
+ case '*':
+ optype = IMMEDIATE_INT;
+ break;
+ case '|':
+ case '&':
+ optype = IMMEDIATE_BOOL;
+ break;
+ default:
+ optype = IMMEDIATE_NO; //ERROR
+ break;
+ }
+
+ return optype;
+ }
+
+ private int getReturnType() {
+ int optype;
+
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_NO) {
+ return leaf.getAttributeType();
+ } else {
+ return isImmediateValue;
+ }
+ }
+
+ switch (operator) {
+ case '-':
+ case '+':
+ case '/':
+ case '*':
+ optype = IMMEDIATE_INT;
+ break;
+ case '|':
+ case '&':
+ case '=':
+ case '$':
+ case '<':
+ case '>':
+ case ':':
+ case ';':
+ optype = IMMEDIATE_BOOL;
+ break;
+ default:
+ optype = IMMEDIATE_NO; //ERROR
+ break;
+ }
+
+ return optype;
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index fe45abd0efd6b4e3aa20a562ae7191d626c80f58..76af8022964d816583229c0b5a7b78608b8086f1 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -111,7 +111,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private SpecificationReinit initState;
//Debug counterexample
- //private boolean counterexample;
+ private boolean counterexample;
+ private CounterexampleTrace counterTrace;
+ public Map<Integer, CounterexampleTraceState> traceStates;
+ private StringBuilder counterTraceReport;
//RG limits
private boolean stateLimitRG;
@@ -144,6 +147,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
timeLimitRG = false;
stateLimit = Integer.MAX_VALUE;
timeLimit = 500;
+ counterexample = false;
freeIntermediateStateCoding = true;
}
@@ -341,6 +345,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
return false;
}
+
+ public void setCounterExampleTrace(boolean counterexample) {
+ this.counterexample = counterexample;
+ if (counterexample) {
+ counterTraceReport = new StringBuilder();
+ }
+ }
+
+ public String getCounterTrace() {
+ if (counterTraceReport == null) {
+ return "";
+ }
+ return counterTraceReport.toString();
+ }
public void setComputeRG(boolean _rg) {
computeRG = _rg;
@@ -380,7 +398,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
initModelChecking();
-
+
stateLimitRG = false;
timeLimitRG = false;
emptyTr = ignoreEmptyTransitions;
@@ -398,6 +416,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyLiveness = false;
studyReachability = false;
studyReinit = false;
+
if (studyL) {
studySafety = true;
@@ -405,10 +424,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = true;
for (SafetyProperty sp : livenesses) {
safety = sp;
+// initCounterexample();
startModelChecking(nbOfThreads);
+// generateCounterexample();
deadlocks += nbOfDeadlocks;
resetModelChecking();
- safety.setComputed();
+ if (!stoppedBeforeEnd) {
+ safety.setComputed();
+ }
}
studySafety = false;
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
@@ -426,7 +449,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = false;
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
}
+ initCounterexample();
startModelChecking(nbOfThreads);
+ generateCounterexample();
if (safety.safetyType == SafetyProperty.LEADS_TO) {
// second pass
safety.initLead();
@@ -435,15 +460,19 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (SpecificationState state : safetyLeadStates.values()) {
deadlocks += nbOfDeadlocks;
resetModelChecking();
+ initCounterexample();
startModelChecking(state, nbOfThreads);
if (safety.result == false) {
+ generateCounterexample();
break;
}
}
System.out.println("Dimensions of lead states to elaborate: " + safetyLeadStates.size());
safetyLeadStates = null;
}
- safety.setComputed();
+ if (!stoppedBeforeEnd) {
+ safety.setComputed();
+ }
deadlocks += nbOfDeadlocks;
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
resetModelChecking();
@@ -492,7 +521,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = studyS;
studyReachability = studyR;
studyReinit = studyRI;
-
+
TraceManager.addDev("Model checking done");
return true;
}
@@ -882,6 +911,26 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
+
+ private void initCounterexample() {
+ if (counterexample) {
+ counterTrace = new CounterexampleTrace(spec);
+ traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ }
+ }
+
+
+ private void generateCounterexample() {
+ if (counterexample && counterTrace.hasCounterexample()) {
+ counterTrace.buildTrace();
+ if (studySafety) {
+ counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
+ counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n");
+ }
+ }
+ }
+
+
private void prepareTransitionsOfState(SpecificationState _ss) {
int cpt;
@@ -923,6 +972,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (_ss.transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
+ checkPropertyOnDeadlock(_ss);
mustStop();
return;
}
@@ -980,7 +1030,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (transitions.size() == 0) {
checkPropertyOnDeadlock(_ss);
nbOfDeadlocks++;
- propertyDone = deadlockStop; //use this flag to stop the execution
//TraceManager.addDev("Deadlock found");
}
@@ -1153,7 +1202,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (newState.transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
- propertyDone = deadlockStop; //use this flag to stop the execution
+ checkPropertyOnDeadlock(_ss);
mustStop();
return;
}
@@ -1874,11 +1923,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
private void actionOnProperty(SpecificationState newState, int i, SpecificationState similar, SpecificationState _ss) {
+ boolean cexample = false;
+
if (studySafety) {
if (safety.safetyType == SafetyProperty.ALLTRACES_ALLSTATES) {
if (newState.property) {
propertyDone = true;
safety.result = false;
+ cexample = true;
} else if (similar == null){
pendingStates.add(newState);
}
@@ -1896,10 +1948,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
newState.freeUselessAllocations();
}
} else if (!newState.property) {
- if (!similar.property && stateIsReachableFromState(similar, _ss)) {
+ if (!similar.property && stateIsReachableFromState(similar, _ss) || similar.property) {
//found a loop with true property
propertyDone = true;
safety.result = true;
+ cexample = true;
}
}
} else if (safety.safetyType == SafetyProperty.ALLTRACES_ONESTATE) {
@@ -1916,16 +1969,18 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
newState.freeUselessAllocations();
}
} else if (newState.property == false) {
- if (!similar.property && stateIsReachableFromState(similar, _ss)) {
+ if (!similar.property && stateIsReachableFromState(similar, _ss) || similar.property) {
//found a loop with false property
propertyDone = true;
safety.result = false;
+ cexample = true;
}
}
} else if (safety.safetyType == SafetyProperty.ONETRACE_ONESTATE) {
if (newState.property) {
propertyDone = true;
safety.result = true;
+ cexample = true;
} else if (similar == null) {
pendingStates.add(newState);
}
@@ -1942,29 +1997,59 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
pendingStates.add(newState);
}
}
- }
-
- if (studyReinit && similar != null) {
+ } else if (studyReinit && similar != null) {
if (similar != initState.initState && stateIsReachableFromState(similar, _ss)) {
propertyDone = true;
initState.setResult(false);
+ cexample = true;
+ }
+ }
+
+ if (counterexample) {
+ if (cexample == true) {
+ CounterexampleTraceState cs = new CounterexampleTraceState();
+ if (_ss != null) {
+ cs.initState(newState, traceStates.get(_ss.hashValue));
+ } else {
+ cs.initState(newState, null);
+ }
+ counterTrace.setCounterexample(cs);
+ } else if (similar == null) {
+ CounterexampleTraceState cs = new CounterexampleTraceState();
+ if (_ss != null) {
+ cs.initState(newState, traceStates.get(_ss.hashValue));
+ } else {
+ cs.initState(newState, null);
+ }
+ traceStates.put(cs.hash, cs);
}
}
}
private void checkPropertyOnDeadlock(SpecificationState ss) {
+ boolean cexample = false;
+
if (studySafety) {
if (safety.safetyType == SafetyProperty.ALLTRACES_ONESTATE && ss.property == false) {
propertyDone = true;
safety.result = false;
+ cexample = true;
} else if (safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES && ss.property == false) {
propertyDone = true;
safety.result = true;
+ cexample = true;
}
- }
- if (studyReinit) {
+ } else if (studyReinit) {
propertyDone = true;
initState.setResult(false);
+ cexample = true;
+ } else if (deadlockStop) {
+ propertyDone = true;
+ cexample = true;
+ }
+
+ if (counterexample && cexample == true) {
+ counterTrace.setCounterexample(traceStates.get(ss.hashValue));
}
}
@@ -2162,14 +2247,19 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return "Deadlock check not activeted\n";
}
- String ret;
+ StringBuilder ret = new StringBuilder();
+
+ if (stoppedBeforeEnd) {
+ ret.append("Beware: Full deadlock study might not have been fully completed\n");
+ }
+
if (nbOfDeadlocks > 0) {
- ret = "property is NOT satisfied\n";
+ ret.append("property is NOT satisfied\n");
} else {
- ret = "property is satisfied\n";
+ ret.append("property is satisfied\n");
}
- return ret;
+ return ret.toString();
}
public String safetyToString() {
@@ -2195,14 +2285,18 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return "Reinitialization check not activeted\n";
}
- String ret;
+ StringBuilder ret = new StringBuilder();
+
+ if (stoppedBeforeEnd) {
+ ret.append("Beware: Full study of liveness might not have been fully completed\n");
+ }
if (initState.getResult()) {
- ret = "property is satisfied\n";
+ ret.append("property is satisfied\n");
} else {
- ret = "property is NOT satisfied\n";
+ ret.append("property is NOT satisfied\n");
}
- return ret;
+ return ret.toString();
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
new file mode 100644
index 0000000000000000000000000000000000000000..aad9fadbd34068c75a2611824b690c9ad86f00e5
--- /dev/null
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -0,0 +1,139 @@
+package avatartranslator.modelchecker;
+
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+
+import avatartranslator.AvatarBlock;
+import avatartranslator.AvatarSpecification;
+import avatartranslator.AvatarStateMachine;
+
+public class CounterexampleTrace {
+ private LinkedList<CounterexampleTraceState> trace;
+ private CounterexampleTraceState counterexampleState;
+ private AvatarSpecification spec;
+
+
+ public CounterexampleTrace(AvatarSpecification spec) {
+ this.trace = null;
+ this.counterexampleState = null;
+ this.spec = spec;
+ }
+
+
+ public void setCounterexample(CounterexampleTraceState cs) {
+ this.counterexampleState = cs;
+ }
+
+
+ public boolean hasCounterexample() {
+ return counterexampleState != null;
+ }
+
+
+ public boolean buildTrace(CounterexampleTraceState cs) {
+ counterexampleState = cs;
+ return buildTrace();
+ }
+
+
+ public boolean buildTrace() {
+ if (counterexampleState == null) {
+ return false;
+ }
+
+ trace = new LinkedList<CounterexampleTraceState>();
+
+ CounterexampleTraceState cs = counterexampleState;
+ trace.add(cs);
+
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+
+ return true;
+ }
+
+
+ public String toString() {
+ if (trace == null) {
+ return "";
+ }
+
+ StringBuilder s = new StringBuilder();
+
+ for (CounterexampleTraceState cs : trace) {
+ s.append(cs.toString() + " -> ");
+ }
+ s.append(" []");
+ return s.toString();
+ }
+
+
+ public String generateSimpleTrace() {
+ if (trace == null) {
+ return "";
+ }
+
+ StringBuilder s = new StringBuilder();
+ List<AvatarBlock> blocks = spec.getListOfBlocks();
+
+ for (AvatarBlock block : blocks) {
+ if (block.getStateMachine().allStates == null) {
+ return "";
+ }
+ }
+
+ int id = 0;
+ for (CounterexampleTraceState cs : trace) {
+ s.append(id);
+ int j = 0;
+ for (AvatarBlock block : blocks) {
+ s.append("\t" + block.getName() + "." + block.getStateMachine().allStates[cs.blocksStates[j++]].getName());
+ }
+ s.append("\n");
+ id++;
+ }
+ return s.toString();
+ }
+
+
+ public String generateSimpleTrace(Map<Integer, SpecificationState> states) {
+ if (trace == null) {
+ return "";
+ }
+
+ StringBuilder s = new StringBuilder();
+ List<AvatarBlock> blocks = spec.getListOfBlocks();
+
+ for (AvatarBlock block : blocks) {
+ if (block.getStateMachine().allStates == null) {
+ return "";
+ }
+ }
+
+ int id = 0;
+ SpecificationState state = null;
+ for (CounterexampleTraceState cs : trace) {
+ if (state != null) {
+ for (SpecificationLink sl : state.nexts) {
+ if (sl.destinationState.hashValue == cs.hash) {
+ s.append("Transition " + sl.action + "\n");
+ break;
+ }
+ }
+ }
+ s.append("State " + id + ":\t");
+ int j = 0;
+ for (AvatarBlock block : blocks) {
+ s.append("\t" + block.getName() + "." + block.getStateMachine().allStates[cs.blocksStates[j++]].getName());
+ }
+ s.append("\n");
+ state = states.get(cs.hash);
+ id++;
+ }
+ return s.toString();
+ }
+
+}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTraceState.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTraceState.java
new file mode 100644
index 0000000000000000000000000000000000000000..d9f0618469e5e6f1348954583abddc5557d52d32
--- /dev/null
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTraceState.java
@@ -0,0 +1,29 @@
+package avatartranslator.modelchecker;
+
+
+public class CounterexampleTraceState {
+ public CounterexampleTraceState father;
+ public int[] blocksStates;
+ public int hash;
+
+ public CounterexampleTraceState() {
+ this.father = null;
+ this.blocksStates = null;
+ }
+
+ public void initState(SpecificationState ss, CounterexampleTraceState father) {
+ this.father = father;
+ this.hash = ss.hashValue;
+ if (ss.blocks != null) {
+ this.blocksStates = new int[ss.blocks.length];
+ for (int i = 0; i < ss.blocks.length; i++) {
+ this.blocksStates[i] = ss.blocks[i].values[SpecificationBlock.STATE_INDEX];
+ }
+ }
+ }
+
+ public String toString() {
+ return "" + hash;
+ }
+
+}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 7392044a6411c77f7e6e057d94f08175dbb1fb81..b3ccbac29ac0767789a92bb8ee4b8f6790432e52 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -49,6 +49,7 @@ import myutil.*;
import ui.util.IconManager;
import ui.MainGUI;
import ui.TGComponent;
+import ui.avatarbd.AvatarBDSafetyPragma;
import graph.RG;
import graph.AUTGraph;
@@ -103,6 +104,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean checkNoDeadSelected = false;
protected static boolean checkReinitSelected = false;
protected static boolean limitStatesSelected = false;
+ protected static boolean generateCountertraceSelected = false;
+ protected static String countertracePath;
protected static String stateLimitValue;
protected static boolean limitTimeSelected = false;
protected static String timeLimitValue;
@@ -154,6 +157,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JCheckBox noDeadlocks;
protected JCheckBox reinit;
protected JCheckBox safety;
+ protected JCheckBox countertrace;
+ protected JTextField countertraceField;
protected JButton checkUncheckAllPragmas;
protected java.util.List<JCheckBox> customChecks;
@@ -190,6 +195,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
graphDirDot = _graphDir + File.separator + "rgavatar$.dot";
}
+ countertracePath = "trace$.txt";
stateLimitValue = "100";
timeLimitValue = "5000";
@@ -442,7 +448,18 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
cadvanced.gridwidth = GridBagConstraints.REMAINDER; //end row
jpadvanced.add(jsp, cadvanced);
}
+ cadvanced.gridwidth = GridBagConstraints.REMAINDER;
+ //Countertrace
+ cadvanced.gridwidth = 1;
+ countertrace = new JCheckBox("Generate counterexample traces", generateCountertraceSelected);
+ countertrace.addActionListener(this);
+ jpadvanced.add(countertrace, cadvanced);
+ cadvanced.gridwidth = GridBagConstraints.REMAINDER;
+ countertraceField = new JTextField(countertracePath);
+ jpadvanced.add(countertraceField, cadvanced);
+
+
jpopt.add(jp01, c01);
jpopt.add(jpbasic, cbasic);
jpopt.add(jpadvanced, cadvanced);
@@ -710,6 +727,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
+ amc.setCounterExampleTrace(generateCountertraceSelected);
// Reachability
int res;
@@ -878,6 +896,23 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
Date date = new Date();
String dateAndTime = dateFormat.format(date);
+
+ if (generateCountertraceSelected) {
+ String trace = amc.getCounterTrace();
+
+ String autfile;
+ if (countertraceField.getText().indexOf("$") != -1) {
+ autfile = Conversion.replaceAllChar(countertraceField.getText(), '$', dateAndTime);
+ } else {
+ autfile = countertraceField.getText();
+ }
+ try {
+ FileUtils.saveFile(autfile, trace);
+ jta.append("\nCounterexample trace saved in " + autfile + "\n");
+ } catch (Exception e) {
+ jta.append("\nCounterexample trace could not be saved in " + autfile + "\n");
+ }
+ }
if (saveGraphAUT.isSelected()) {
graphAUT = amc.toAUT();
@@ -992,9 +1027,11 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
for (SafetyProperty sp : safeties) {
if (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) {
- status = 1;
+ status = AvatarBDSafetyPragma.PROVED_TRUE;
+ } else if (sp.getPhase() == SpecificationPropertyPhase.NONSATISFIED) {
+ status = AvatarBDSafetyPragma.PROVED_FALSE;
} else {
- status = 0;
+ status = AvatarBDSafetyPragma.PROVED_ERROR;
}
verifMap.put(sp.getRawProperty(), status);
}
@@ -1044,6 +1081,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
+ countertrace.setEnabled(safety.isSelected());
+ countertraceField.setEnabled(countertrace.isSelected());
+ generateCountertraceSelected = countertrace.isSelected();
+
stateLimitField.setEnabled(stateLimit.isSelected());
limitStatesSelected = stateLimit.isSelected();
timeLimitField.setEnabled(timeLimit.isSelected());
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index fc7a80c38a7cd7eb8b03c65d8a960d3561d8aeac..96318fb4bcb1b693fc76f949b32f1e07511d709b 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -76,10 +76,16 @@ public class AvatarExpressionTest {
block1.addAttribute(y1);
AvatarAttribute z1 = new AvatarAttribute("z", AvatarType.INTEGER, block1, null);
block1.addAttribute(z1);
+ AvatarAttribute a1 = new AvatarAttribute("key1", AvatarType.BOOLEAN, block1, null);
+ block1.addAttribute(a1);
+ AvatarAttribute b1 = new AvatarAttribute("key2", AvatarType.BOOLEAN, block1, null);
+ block1.addAttribute(b1);
x1.setInitialValue("10");
y1.setInitialValue("5");
z1.setInitialValue("2");
+ a1.setInitialValue("true");
+ b1.setInitialValue("false");
block2 = new AvatarBlock("block2", as, null);
as.addBlock(block2);
@@ -98,38 +104,78 @@ public class AvatarExpressionTest {
@Test
public void testImmediate() {
AvatarExpressionSolver e1 = new AvatarExpressionSolver("10 + 15 >= 20");
- e1.buildExpression();
+ assertTrue(e1.buildExpression());
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-10 / 2 - 15 * 2 + 1 == -30 -4");
- e2.buildExpression();
+ assertTrue(e2.buildExpression());
AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-10 / 2 - 15 * 2 + 1 == -(60 - 26))");
- e3.buildExpression();
+ assertTrue(e3.buildExpression());
AvatarExpressionSolver e4 = new AvatarExpressionSolver("1 && 0 >= 1 || 0");
- e4.buildExpression();
+ assertFalse(e4.buildExpression());
AvatarExpressionSolver e5 = new AvatarExpressionSolver("true and not(false) == not(false or false)");
- e5.buildExpression();
+ assertTrue(e5.buildExpression());
AvatarExpressionSolver e6 = new AvatarExpressionSolver("10 -Cabin.match");
+ assertFalse(e6.buildExpression());
+ AvatarExpressionSolver e7 = new AvatarExpressionSolver("not(10)");
+ assertFalse(e7.buildExpression());
+ AvatarExpressionSolver e8 = new AvatarExpressionSolver("-(false)");
+ assertFalse(e8.buildExpression());
+ AvatarExpressionSolver e9 = new AvatarExpressionSolver("-10 < 5 && 20/4 == 5");
+ assertTrue(e9.buildExpression());
+ AvatarExpressionSolver e10 = new AvatarExpressionSolver("true && 0 >= 1 || false");
+ assertTrue(e10.buildExpression());
assertTrue(e1.getResult() == 1);
assertTrue(e2.getResult() == 1);
assertTrue(e3.getResult() == 0);
- assertTrue(e4.getResult() == 0);
assertTrue(e5.getResult() == 1);
- assertTrue(e6.buildExpression() == false);
+ assertTrue(e9.getResult() == 1);
+ assertTrue(e10.getResult() == 0);
}
@Test
public void testBlock() {
SpecificationBlock specBlock = new SpecificationBlock();
specBlock.init(block1, false);
+ int[] attributes = {2, 3, 7, 0, 1};
AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
- e1.buildExpression(block1);
+ assertTrue(e1.buildExpression(block1));
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-x / y - 15 * z + 1 == -31");
- e2.buildExpression(block1);
+ assertTrue(e2.buildExpression(block1));
AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-x / z - (x + y) * 2 + 1 >= -(60 - 26))");
- e3.buildExpression(block1);
+ assertTrue(e3.buildExpression(block1));
+ AvatarExpressionSolver e4 = new AvatarExpressionSolver("(key1==true) and (key2==false)");
+ assertTrue(e4.buildExpression(block1));
+ AvatarExpressionSolver e5 = new AvatarExpressionSolver("(key1) and (key2)");
+ assertTrue(e5.buildExpression(block1));
+ AvatarExpressionSolver e6 = new AvatarExpressionSolver("(key1==key1) or (key2==key1)");
+ assertTrue(e6.buildExpression(block1));
+ AvatarExpressionSolver e7 = new AvatarExpressionSolver("((key1==key1) and not(key2==key1)) and (x - y == z + 3)");
+ assertTrue(e7.buildExpression(block1));
+ AvatarExpressionSolver e8 = new AvatarExpressionSolver("x + x*(y+z)/(x + z - x)");
+ assertTrue(e8.buildExpression(block1));
+ AvatarExpressionSolver e9 = new AvatarExpressionSolver("x + x*(y+z)*(x - z)");
+ assertTrue(e9.buildExpression(block1));
+ AvatarExpressionSolver e10 = new AvatarExpressionSolver("x*((x + y)*z + (x+z)/z)/x");
+ assertTrue(e10.buildExpression(block1));
+ AvatarExpressionSolver e11 = new AvatarExpressionSolver("x + y");
+ assertTrue(e11.buildExpression(block1));
+ AvatarExpressionSolver e12 = new AvatarExpressionSolver("x*((x + y)*z + (x+z)/z)/x");
+ assertTrue(e12.buildExpression(block1));
+ AvatarExpressionSolver e13 = new AvatarExpressionSolver("(key1==false) and (key2==true)");
+ assertTrue(e13.buildExpression(block1));
assertTrue(e1.getResult(specBlock) == 15);
assertTrue(e2.getResult(specBlock) == 1);
assertTrue(e3.getResult(specBlock) == 0);
+ assertTrue(e4.getResult(specBlock) == 1);
+ assertTrue(e5.getResult(specBlock) == 0);
+ assertTrue(e6.getResult(specBlock) == 1);
+ assertTrue(e7.getResult(specBlock) == 1);
+ assertTrue(e8.getResult(specBlock) == 45);
+ assertTrue(e9.getResult(specBlock) == 570);
+ assertTrue(e10.getResult(specBlock) == 36);
+ assertTrue(e11.getResult(attributes) == 5);
+ assertTrue(e12.getResult(attributes) == 36);
+ assertTrue(e13.getResult(attributes) == 1);
}
@Test
@@ -138,11 +184,11 @@ public class AvatarExpressionTest {
ss.setInit(as, false);
AvatarExpressionSolver e1 = new AvatarExpressionSolver("block1.x + block2.y");
- e1.buildExpression(as);
+ assertTrue(e1.buildExpression(as));
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-block1.x / block1.y - 15 * block2.z + 1 == -46");
- e2.buildExpression(as);
+ assertTrue(e2.buildExpression(as));
AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-block2.x / block2.z - not(block1.x + block2.y) * -2 + -(1) <= -(-4 + 7))");
- e3.buildExpression(as);
+ assertFalse(e3.buildExpression(as));
assertTrue(e1.getResult(ss) == 17);
assertTrue(e2.getResult(ss) == 1);
assertTrue(e3.getResult(ss) == 0);