Commit 3c1650c7 authored by Ludovic Apvrille's avatar Ludovic Apvrille

Merge branch 'model_checker' into 'master'

Model-checker to merge

See merge request !328
parents 05297783 5b3f25ec
# Tools
LATEXFLAGS ?= -interaction=nonstopmode -file-line-error
PDFLATEX = pdflatex $(LATEXFLAGS)
BIBTEX =
FIG2DEV = fig2dev
RUBBER ?= $(shell which rubber 2> /dev/null)
RUBBERFLAGS = --pdf --short --warn refs --warn misc
# Files and directories
FIGDIR = figures
FIGS = $(wildcard $(FIGDIR)/*.fig)
FIGPDFS = $(patsubst $(FIGDIR)/%.fig,$(FIGDIR)/%.pdf,$(FIGURES))
FIGPDFTS = $(patsubst $(FIGDIR)/%.fig,$(FIGDIR)/%.pdf_t,$(FIGURES))
FIGURES = $(filter-out $(FIGS) $(FIGPDFS) $(FIGPDFTS), $(wildcard $(FIGDIR)/*))
JOB = ttool_avatarmodelchecker
TEXS = $(wildcard *.tex) $(wildcard *.sty) $(wildcard *.cls)
PICS = $(wildcard *.png) $(filter-out $(JOB).pdf,$(wildcard *.pdf))
BIBS = $(wildcard *.bib) $(wildcard *.bst)
TOPS = $(shell grep -l '[^%]*\\begin{document}' *.tex)
PDFTARGETS = $(patsubst %.tex,%.pdf,$(TOPS))
TARGETS = $(patsubst %.tex,%,$(TOPS))
.DEFAULT: help
.PHONY: all help clean ultraclean
help:
@echo '----------------------------------------------------------------'; \
echo 'available targets:'; \
echo ' "make" or "make help": print this help'; \
echo ' "make foo" or "make foo.pdf": build the foo.pdf document'; \
echo ' "make all": build all documents'; \
echo ' "make clean": delete non-essential generated files'; \
echo ' "make ultraclean": delete all generated files'; \
echo '----------------------------------------------------------------'; \
echo 'Buildable documents:'; \
echo -n $(sort $(TARGETS)) | sed -e 's/\([^ ]\+\) */ \1\n/g'; \
echo '----------------------------------------------------------------'; \
echo 'if you encounter problems please contact:'; \
echo ' Renaud Pacalet <renaud.pacalet@telecom-paristech.fr>'; \
echo '----------------------------------------------------------------'
all: $(PDFTARGETS)
$(TARGETS): % : %.pdf
ifeq ($(RUBBER),)
# Bootstrap aux file, then keep running pdflatex until it reaches a fixpoint
$(JOB).aux: | $(TEXS) $(PICS)
$(PDFLATEX) $(JOB)
$(JOB).bbl: $(JOB).aux $(BIBS)
$(BIBTEX) $(JOB)
$(JOB).pdf: $(TEXS) $(PICS) $(JOB).aux $(JOB).bbl
@cp -p $(JOB).aux $(JOB).aux.bak
$(PDFLATEX) $(JOB)
@if cmp -s $(JOB).aux $(JOB).aux.bak; \
then touch -r $(JOB).aux.bak $(JOB).aux; \
else NEWS="$$NEWS -W $(JOB).aux"; fi; rm $(JOB).aux.bak; \
if [ -n "$$NEWS" ]; then $(MAKE) $$NEWS $@; fi
$(FIGDIR)/%.pdf: $(FIGDIR)/%.fig
$(FIG2DEV) -L pdftex $< $@
$(FIGDIR)/%.pdf_t: $(FIGDIR)/%.fig $(FIGDIR)/%.pdf
$(FIG2DEV) -L pdftex_t -p $(patsubst %.pdf_t,%.pdf,$@) $< $@
clean:
rm -f $(JOB).aux $(JOB).log $(JOB).blg $(JOB).bbl $(JOB).out $(JOB).pdf
else
.NOTPARALLEL:
.PHONY: $(PDFTARGETS)
$(PDFTARGETS): %.pdf: %.tex
@$(RUBBER) $(RUBBERFLAGS) $<
clean:
@$(RUBBER) $(RUBBERFLAGS) --clean $(TOPS)
endif
This diff is collapsed.
......@@ -42,6 +42,8 @@ import myutil.TraceManager;
import java.util.Map;
import avatartranslator.modelchecker.SpecificationBlock;
/**
* Class AvatarActionAssignment
* Creation: 16/09/2015
......@@ -51,10 +53,14 @@ import java.util.Map;
public class AvatarActionAssignment implements AvatarAction {
AvatarLeftHand leftHand;
AvatarTerm rightHand;
AvatarExpressionSolver actionSolver;
private AvatarExpressionAttribute leftAttribute;
public AvatarActionAssignment (AvatarLeftHand _leftHand, AvatarTerm _rightHand) {
this.leftHand = _leftHand;
this.rightHand = _rightHand;
this.actionSolver = null;
this.leftAttribute = null;
}
public boolean isAVariableSetting () {
......@@ -72,6 +78,10 @@ public class AvatarActionAssignment implements AvatarAction {
public AvatarTerm getRightHand () {
return this.rightHand;
}
public AvatarExpressionSolver getActionSolver() {
return actionSolver;
}
public boolean isABasicVariableSetting () {
return (this.leftHand instanceof AvatarAttribute || this.leftHand instanceof AvatarTuple) &&
......@@ -85,6 +95,19 @@ public class AvatarActionAssignment implements AvatarAction {
public String toString () {
return this.leftHand.getName() + " = " + this.rightHand.getName();
}
public boolean buildActionSolver(AvatarBlock block) {
boolean res;
actionSolver = new AvatarExpressionSolver(rightHand.getName());
res = actionSolver.buildExpression((AvatarBlock) block);
leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName());
res &= !leftAttribute.hasError();
return res;
}
public void executeActionSolver(SpecificationBlock sb) {
leftAttribute.setValue(sb, actionSolver.getResult(sb));
}
@Override
public boolean containsAMethodCall () {
......
......@@ -41,6 +41,7 @@ package avatartranslator;
import myutil.TraceManager;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
......@@ -55,6 +56,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
private AvatarSignal signal;
private List<String> values;
private boolean checkLatency;
private List<AvatarExpressionAttribute> actionAttr;
public AvatarActionOnSignal(String _name, AvatarSignal _signal, Object _referenceObject ) {
......@@ -69,6 +71,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
signal = _signal;
values = new LinkedList<String>();
actionAttr = null;
}
public AvatarSignal getSignal() {
......@@ -106,6 +109,23 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
public boolean isReceiving() {
return signal.isIn();
}
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);
actionAttr.add(aea);
res &= aea.hasError();
}
return res;
}
public AvatarExpressionAttribute getExpressionAttribute(int index) {
return actionAttr.get(index);
}
public AvatarActionOnSignal basicCloneMe(AvatarStateMachineOwner _block) {
//TraceManager.addDev("I HAVE BEEN CLONED: " + this);
......
......@@ -57,6 +57,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
private List<AvatarSignal> signals;
private AvatarStateMachine asm;
private AvatarSpecification avspec;
private int blockIndex; //Index of block in the Avatar Specification
private String globalCode;
......@@ -253,6 +254,14 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public AvatarAttribute getAttribute(int _index) {
return attributes.get(_index);
}
public int getBlockIndex() {
return blockIndex;
}
public void setBlockIndex(int _blockIndex) {
blockIndex = _blockIndex;
}
public boolean setAttributeValue(int _index, String _value) {
AvatarAttribute aa = attributes.get(_index);
......
/* 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;
import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState;
/**
* Class AvatarExpressionAttribute
* Avatar Expression Attribute
* Creation: 17/04/2020
*
* @author Alessandro TEMPIA CALVINO
* @version 1.0 17/04/2020
*/
public class AvatarExpressionAttribute {
private AvatarBlock block;
private int blockIndex;
private int accessIndex;
private AvatarStateMachineElement state;
private String s;
private boolean isState;
private boolean error;
public AvatarExpressionAttribute(AvatarSpecification spec, String s) {
this.s = s;
isState = false;
error = !initAttributes(spec);
}
public AvatarExpressionAttribute(AvatarBlock block, String s) {
this.s = s;
isState = false;
error = !initAttributes(block);
}
public AvatarExpressionAttribute(AvatarBlock block, AvatarStateMachineElement asme) {
this.s = asme.name;
isState = true;
state = asme;
error = false;
}
private boolean initAttributes(AvatarSpecification spec) {
//Extract Block and Attribute
String[] splitS;
String blockString;
String fieldString;
if (spec == null) {
return false;
}
if (s.matches(".+\\..+")) {
splitS = s.split("\\.");
blockString = splitS[0];
fieldString = splitS[1];
} else {
return false;
}
block = spec.getBlockWithName(blockString);
if (blockIndex == -1) {
return false;
}
blockIndex = spec.getBlockIndex(block);
int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
if (attributeIndex == -1) {
// state?
state = block.getStateMachine().getStateWithName(fieldString);
if (state == null) {
return false;
}
isState = true;
}
accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
return true;
}
private boolean initAttributes(AvatarBlock block) {
//Extract Attribute
if (block == null) {
return false;
}
this.block = block;
this.blockIndex = -1; //not initialized
int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
if (attributeIndex == -1) {
// state?
state = block.getStateMachine().getStateWithName(s);
if (state == null) {
return false;
}
isState = true;
}
accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
return true;
}
public boolean hasError() {
return error == true;
}
public int getValue(SpecificationState ss) {
int value;
if (isState) {
return 0;
}
value = ss.blocks[blockIndex].values[accessIndex];
return value;
}
public int getValue(SpecificationState ss, AvatarStateMachineElement asme) {
int value;
if (isState) {
return (state == asme) ? 1 : 0;
}
value = ss.blocks[blockIndex].values[accessIndex];
return value;
}
public int getValue(SpecificationBlock sb) {
int value;
if (isState) {
return 0;
}
value = sb.values[accessIndex];
return value;
}
public void setValue(SpecificationState ss, int value) {
int v;
if (isState) {
return;
}
v = value;
ss.blocks[blockIndex].values[accessIndex] = v;
}
public void setValue(SpecificationBlock sb, int value) {
int v;
if (isState) {
return;
}
v = value;
sb.values[accessIndex] = v;
}
public boolean isState() {
return isState;
}
public String toString() {
return s;
}
}
This diff is collapsed.
......@@ -304,6 +304,18 @@ public class AvatarSpecification extends AvatarElement {
return null;
}
public int getBlockIndex(AvatarBlock _block) {
int cpt = 0;
for(AvatarBlock block: blocks) {
if (block == _block) {
return cpt;
}
cpt++;
}
return -1;
}
public AvatarAMSInterface getAMSInterfaceWithName(String _name) {
for(AvatarAMSInterface interf: interfaces) {
......
......@@ -44,6 +44,7 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
/**
* Class AvatarTransition
* Creation: 20/05/2010
......@@ -73,6 +74,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
private String minDelay = "", maxDelay = "";
private String minCompute = "", maxCompute = "";
private AvatarStateMachineOwner block;
private AvatarExpressionSolver guardSolver;
private List<AvatarAction> actions; // actions on variable, or method call
......@@ -81,11 +84,23 @@ public class AvatarTransition extends AvatarStateMachineElement {
actions = new LinkedList<AvatarAction>();
this.guard = new AvatarGuardEmpty();
this.block = _block;
guardSolver = null;
}
public AvatarGuard getGuard() {
return guard;
}
public boolean buildGuardSolver() {
String expr = guard.toString().replaceAll("\\[", "").trim();
expr = expr.replaceAll("\\]", "");
guardSolver = new AvatarExpressionSolver(expr);
return guardSolver.buildExpression((AvatarBlock) block);
}
public AvatarExpressionSolver getGuardSolver() {
return guardSolver;
}
public void setGuard(AvatarGuard _guard) {
this.guard = _guard;
......
......@@ -36,10 +36,6 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
package avatartranslator.modelchecker;
import avatartranslator.*;
......@@ -47,91 +43,251 @@ import avatartranslator.*;
/**
* Class SafetyProperty
* Coding of a ssafety property
* Coding of a safety property
* Creation: 22/11/2017
* @version 1.0 22/11/2017
* @author Ludovic APVRILLE
*/
public class SafetyProperty {
private String rawProperty;
private int errorOnProperty;
private AvatarExpressionSolver safetySolver;
private AvatarExpressionSolver safetySolverLead;
private SpecificationPropertyPhase phase;
private AvatarStateMachineElement state;
// Error on property
public static final int NO_ERROR = 0;
public static final int BAD_SAFETY_TYPE = 1;
public static final int BAD_PROPERTY_STRUCTURE = 1;
// Type of safety
public static final int ALLTRACES_ALLSTATES = 0;// A[]
public static final int ALLTRACES_ONESTATE = 1; // A<>
public static final int ONETRACE_ALLSTATES = 2; // E[]
public static final int ONETRACE_ONESTATE = 3; // E<>
public static final int ALLTRACES_ALLSTATES = 0;// A[] p
public static final int ALLTRACES_ONESTATE = 1; // A<> p
public static final int ONETRACE_ALLSTATES = 2; // E[] p
public static final int ONETRACE_ONESTATE = 3; // E<> p
public static final int LEADS_TO = 4; // p --> q
// Type of property
public static final int BLOCK_STATE = 0;
public static final int BOOL_EXPR = 1;
public int safetyType;
public int propertyType;
public int leadType;
public boolean result;
private String rawProperty;
private int safetyType;
private int propertyType;
private String p;
private boolean isBlockStateProperty;
private int blockIndex;
private int stateIndex;
private int errorOnProperty;
public SafetyProperty(String property, AvatarSpecification _spec) {
rawProperty = property.trim();
analyzeProperty(_spec);
rawProperty = property.trim();
analyzeProperty(_spec);
phase = SpecificationPropertyPhase.NOTCOMPUTED;
}
public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state, int _safetyType) {
//create liveness safety
AvatarExpressionAttribute attribute = new AvatarExpressionAttribute(block, state);
safetySolver = new AvatarExpressionSolver();
safetySolver.builExpression(attribute);
propertyType = BLOCK_STATE;
safetyType = _safetyType;
result = true;
phase = SpecificationPropertyPhase.NOTCOMPUTED;
rawProperty = "Element " + state.getExtendedName() + " of block " + block.getName();
this.state = state;
}
public boolean analyzeProperty(AvatarSpecification _spec) {
String tmpP = rawProperty;
errorOnProperty = NO_ERROR;
if (tmpP.startsWith("A[]")) {
safetyType = ALLTRACES_ALLSTATES;
} else if (tmpP.startsWith("A<>")) {
safetyType = ALLTRACES_ONESTATE;
} else if (tmpP.startsWith("E[]")) {
safetyType = ONETRACE_ALLSTATES;
} else if (tmpP.startsWith("E<>")) {
safetyType = ONETRACE_ONESTATE;
} else {
errorOnProperty = BAD_SAFETY_TYPE;
return false;
}
p = tmpP.substring(3, tmpP.length()).trim();
if (p.length() == 0) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
return false;
}
return (errorOnProperty == NO_ERROR);
String tmpP = rawProperty;
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;
}
if (safetyType != LEADS_TO) {
p = tmpP.substring(3, tmpP.length()).trim();
initSafetyTrace(_spec, p);
} else {
p = tmpP;
initSafetyLeads(_spec, p);
}
return (errorOnProperty == NO_ERROR);
}
public void initLead() {
safetySolver = safetySolverLead;
safetyType = ALLTRACES_ONESTATE;
propertyType = leadType;
result = true;
}
public boolean hasError() {
return errorOnProperty != NO_ERROR;
return errorOnProperty != NO_ERROR;
}
public void setErrorOnP() {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
errorOnProperty = BAD_PROPERTY_STRUCTURE;
}
public String getP() {
return p;
public String getRawProperty() {
return rawProperty;
}
public boolean getSolverResult(SpecificationState _ss) {
return safetySolver.getResult(_ss) != 0;
}
public boolean getSolverResult(SpecificationState _ss, AvatarStateMachineElement _asme) {
return safetySolver.getResult(_ss, _asme) != 0;
}
public boolean getSolverLeadResult(SpecificationState _ss, AvatarStateMachineElement _asme) {
return safetySolverLead.getResult(_ss, _asme) != 0;
}
public SpecificationPropertyPhase getPhase() {
return phase;
}