Commit c04c841a authored by Ludovic Apvrille's avatar Ludovic Apvrille

Merge branch 'alessandro_branch' into 'master'

Solved bug for safety properties repainting, plus warnings

See merge request !329
parents bd373334 f4282122
......@@ -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);
......
......@@ -283,12 +283,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return reachabilities.size() - nbOfRemainingReachabilities;
}
public int getNbOfDeadlocks() {
return nbOfDeadlocks;
}
public int setSafetyAnalysis() {
safeties = new ArrayList<SafetyProperty>();
if (safeties == null) {
safeties = new ArrayList<SafetyProperty>();
}
for (String property : spec.getSafetyPragmas()) {
SafetyProperty sp = new SafetyProperty(property, spec);
if (!sp.hasError()) {
......@@ -298,6 +302,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = safeties.size() > 0;
return safeties.size();
}
public boolean addSafety(String pragma) {
if (safeties == null) {
safeties = new ArrayList<SafetyProperty>();
}
SafetyProperty sp = new SafetyProperty(pragma, spec);
if (!sp.hasError()) {
safeties.add(sp);
studySafety = true;
return true;
}
return false;
}
public ArrayList<SafetyProperty> getSafeties() {
return safeties;
......
......@@ -80,7 +80,7 @@ public class SafetyProperty {
public SafetyProperty(String property, AvatarSpecification _spec) {
rawProperty = property.trim();
rawProperty = property;
analyzeProperty(_spec);
phase = SpecificationPropertyPhase.NOTCOMPUTED;
}
......@@ -99,7 +99,7 @@ public class SafetyProperty {
}
public boolean analyzeProperty(AvatarSpecification _spec) {
String tmpP = rawProperty;
String tmpP = rawProperty.trim();
String p;
errorOnProperty = NO_ERROR;
......
......@@ -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);
......
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