Commit ecfbd1a0 authored by tempiaa's avatar tempiaa

Merge branch 'model_checker' into alessandro_branch

parents a6e156f4 e6dd15c8
13346
\ No newline at end of file
13397
\ No newline at end of file
......@@ -99,7 +99,7 @@ public class AvatarActionAssignment implements AvatarAction {
public boolean buildActionSolver(AvatarBlock block) {
boolean res;
actionSolver = new AvatarExpressionSolver(rightHand.getName());
res = actionSolver.buildExpression((AvatarBlock) block);
res = actionSolver.buildExpression(block);
leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName());
res &= !leftAttribute.hasError();
return res;
......
......@@ -113,7 +113,6 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
public boolean buildActionSolver(AvatarBlock block) {
AvatarExpressionAttribute aea;
boolean res = true;
int i = 0;
actionAttr = new ArrayList<AvatarExpressionAttribute>();
for (String val : values) {
aea = new AvatarExpressionAttribute(block, val);
......
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT enst.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
package avatartranslator.modelchecker;
/**
* Class SpecificationReachabilityType
* Reachability types
* Creation: 07/06/2016
* @version 1.0 07/06/2016
* @author Ludovic APVRILLE
*/
public enum SpecificationReachabilityType {
NOTCOMPUTED, REACHABLE, NONREACHABLE
}
......@@ -50,8 +50,8 @@ package ui.util;
*/
public class DefaultText {
public static String BUILD = "13345";
public static String DATE = "2020/03/23 03:11:56 CET";
public static String BUILD = "13396";
public static String DATE = "2020/05/13 03:11:56 CET";
public static StringBuffer sbAbout = makeAbout();
......
......@@ -878,6 +878,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
switch (_res) {
case NOTCOMPUTED:
tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
break;
case SATISFIED:
tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment