Commit ee99bb37 authored by Simone Vuotto's avatar Simone Vuotto

Add LTLDcSpec and update the testing environment to support numeric variables

parent d2040197
Pipeline #194 passed with stages
in 2 minutes and 10 seconds
package it.sagelab.specpro.models.ltl;
import it.sagelab.specpro.models.ltl.assign.Assignment;
import it.sagelab.specpro.models.ltl.assign.NumericAssignment;
import it.sagelab.specpro.models.psp.Requirement;
import it.sagelab.specpro.models.psp.expressions.Expression;
import it.sagelab.specpro.models.translators.RangeMapVisitor;
import java.util.*;
public class LTLDcSpec extends LTLSpec {
/** The range map. */
private Map<String, TreeMap<Float, Atom[]>> rangeMap;
public LTLDcSpec(List<? extends Requirement> requirements) {
computeRangeMap(requirements);
}
public Map<String, TreeMap<Float, Atom[]>> getRangeMap() {
return rangeMap;
}
/**
* Gets the lists of thresholds in ascending order defined for the given variable.
* @param varName the name of the variable.
* @return a sorted list of thresholds.
*/
public List<Float> getThresholds(String varName) {
ArrayList<Float> thresholds = new ArrayList<>();
NavigableSet<Float> keys = rangeMap.get(varName).navigableKeySet();
for(Float f: keys) {
thresholds.add(f);
}
return thresholds;
}
/**
* Gets the set of numeric variable names used in the specification
* @return the set of numeric variable names
*/
public Set<String> getNumericVariableNames() {
return rangeMap.keySet();
}
/**
* Returns the right assignments of LTL(Dc) boolean variables given the numerical assignment of a variable.
* @param var the numeric variable name
* @param value the value assigned to the variable
* @return the corresponding boolean assignment (with the extendend LTL(Dc) boolean variables)
*/
public Assignment getDcAssignment(String var, Float value) {
Assignment assignment = new Assignment();
Float prev = Float.NEGATIVE_INFINITY;
NavigableSet<Float> keys = rangeMap.get(var).navigableKeySet();
for(Float f: keys) {
Atom[] atoms = rangeMap.get(var).get(f);
assignment.add(atoms[0], value.compareTo(prev) > 0 && value.compareTo(f) < 0);
assignment.add(atoms[1], value.compareTo(f) == 0);
prev = f;
}
return assignment;
}
public Float[] getRangeFromDcAssignment(String var, Assignment assignment) {
Float prev = Float.NEGATIVE_INFINITY;
NavigableSet<Float> keys = rangeMap.get(var).navigableKeySet();
for(Float f: keys) {
Atom[] atoms = rangeMap.get(var).get(f);
if(assignment.contains(atoms[0]) || assignment.contains(atoms[1])) {
if(assignment.contains(atoms[0]) && assignment.getValue(atoms[0])) {
return new Float[] {prev, f};
}
if(assignment.contains(atoms[1]) && assignment.getValue(atoms[1])) {
return new Float[] {f};
}
prev = f;
}
}
return new Float[]{prev, Float.POSITIVE_INFINITY};
}
public NumericAssignment fromBool2Numeric(Assignment assignment) {
NumericAssignment na = new NumericAssignment();
HashMap<String, Assignment> numericAssignments = new HashMap<>();
for(Atom a: assignment.getAssignments().keySet()) {
if(a.getProperty(Atom.PROPERTY_NUMERIC) == null) {
na.add(a, assignment.getValue(a));
} else {
numericAssignments.putIfAbsent((String) a.getProperty(Atom.PROPERTY_NUMERIC_VAR), new Assignment());
numericAssignments.get(a.getProperty(Atom.PROPERTY_NUMERIC_VAR)).add(a, assignment.getValue(a));
}
}
for(Map.Entry<String, Assignment> entry: numericAssignments.entrySet()) {
Float[] range = getRangeFromDcAssignment(entry.getKey(), entry.getValue());
if(range.length < 2) {
na.add(new Atom(entry.getKey()), range[0]);
} else {
na.add(new Atom(entry.getKey()), (range[0] + range[1]) / 2);
}
}
return na;
}
public Assignment fromNumeric2Bool(NumericAssignment numericAssignment) {
Assignment assignment = new Assignment(numericAssignment);
for(Map.Entry<Atom, Float> entry: numericAssignment.getFloatAssignments().entrySet()) {
assignment.add(getDcAssignment(entry.getKey().getName(), entry.getValue()));
}
return assignment;
}
/**
* Gets the equal atom.
*
* @param varName the var name
* @param threshold the threshold
* @return the equal atom
*/
public Atom getEqualAtom(String varName, Float threshold) {
return rangeMap.get(varName).get(threshold)[1];
}
/**
* Gets the lower atom.
*
* @param varName the var name
* @param threshold the threshold
* @return the lower atom
*/
public Atom getLowerAtom(String varName, Float threshold) {
return rangeMap.get(varName).get(threshold)[0];
}
/**
* Compute range map.
*
* @param requirements the psp
*/
private void computeRangeMap(List<? extends Requirement> requirements){
RangeMapVisitor rangeMapVisitor = new RangeMapVisitor();
for(Requirement r : requirements) {
for (Expression e : r.getScope().getExpressions())
e.accept(rangeMapVisitor);
for (Expression e : r.getExpressions())
e.accept(rangeMapVisitor);
}
rangeMap = rangeMapVisitor.getRangeMap();
}
}
package it.sagelab.specpro.models.ltl.assign;
import it.sagelab.specpro.models.ltl.Atom;
import java.util.HashMap;
import java.util.Map;
public class NumericAssignment extends Assignment {
private final HashMap<Atom, Float> numericAssignmentsMap;
public NumericAssignment() {
numericAssignmentsMap = new HashMap<>();
}
public void add(Atom a, Float value) {
if(numericAssignmentsMap.containsKey(a)) {
if(numericAssignmentsMap.get(a) != value) {
throw new IllegalArgumentException("Atom " + a.getName() + " has already a different value");
}
} else {
numericAssignmentsMap.put(a, value);
}
}
public Map<Atom, Float> getFloatAssignments() {
return numericAssignmentsMap;
}
}
......@@ -20,10 +20,7 @@ public class PSP2LTL implements ExpressionVisitor {
/** The patterns map. */
private static final Map<String, Pattern> patternMap = Pattern.loadPatterns(Pattern.PATTERNS_FILE);
private LTLSpec spec;
/** The range map. */
private Map<String, TreeMap<Float, Atom[]>> rangeMap;
private LTLDcSpec spec;
/** The formula. */
private Formula formula;
......@@ -32,11 +29,9 @@ public class PSP2LTL implements ExpressionVisitor {
}
public LTLSpec translate(List<? extends Requirement> requirements) {
rangeMap = computeRangeMap(requirements);
PatternUnifier patternUnifier = new PatternUnifier();
spec = new LTLSpec();
spec = new LTLDcSpec(requirements);
for(Requirement r : requirements) {
Pattern pattern = patternMap.get(r.key());
......@@ -54,7 +49,7 @@ public class PSP2LTL implements ExpressionVisitor {
spec.addInvariant(i);
}
for(TreeMap<Float, Atom[]> map: rangeMap.values()) {
for(TreeMap<Float, Atom[]> map: spec.getRangeMap().values()) {
for(Atom[] atoms : map.values()) {
spec.getSymbolTable().put(atoms[0].getLabel(), atoms[0]);
spec.getSymbolTable().put(atoms[1].getLabel(), atoms[1]);
......@@ -71,8 +66,8 @@ public class PSP2LTL implements ExpressionVisitor {
*/
private List<Formula> getInvariants() {
ArrayList<Formula> invariants = new ArrayList<>();
for(String varName : rangeMap.keySet()) {
TreeMap<Float, Atom[]> rangesToAtoms = rangeMap.get(varName);
for(String varName : spec.getRangeMap().keySet()) {
TreeMap<Float, Atom[]> rangesToAtoms = spec.getRangeMap().get(varName);
// With LOWER_EQUAL and the last key, all the Atoms associated with the variables are returned
List<Atom> variables = getAtoms(varName,rangesToAtoms.lastKey(),CompareExpression.Operator.LOWER_EQUAL);
for (int i = 0; i < variables.size()-1; i++) {
......@@ -175,23 +170,6 @@ public class PSP2LTL implements ExpressionVisitor {
public void visitNumberExpression(NumberExpression exp) { }
/**
* Compute range map.
*
* @param requirements the psp
* @return the map
*/
private static Map<String, TreeMap<Float, Atom[]>> computeRangeMap(List<? extends Requirement> requirements){
RangeMapVisitor rangeMapVisitor = new RangeMapVisitor();
for(Requirement r : requirements) {
for (Expression e : r.getScope().getExpressions())
e.accept(rangeMapVisitor);
for (Expression e : r.getExpressions())
e.accept(rangeMapVisitor);
}
return rangeMapVisitor.getRangeMap();
}
/**
* Gets the ltl formula from the numerical constraint.
*
......@@ -203,9 +181,9 @@ public class PSP2LTL implements ExpressionVisitor {
private Formula getFormulaFromConstraint(String varName, Float threshold, CompareExpression.Operator operator) {
Formula f = null;
if (operator == CompareExpression.Operator.EQUAL) {
f = getEqualAtom(varName, threshold);
f = spec.getEqualAtom(varName, threshold);
} else if(operator == CompareExpression.Operator.NOT_EQUAL) {
f = new UnaryOperator(getEqualAtom(varName, threshold), UnaryOperator.Operator.NOT);
f = new UnaryOperator(spec.getEqualAtom(varName, threshold), UnaryOperator.Operator.NOT);
} else {
List<Atom> variables = getAtoms(varName,threshold,operator);
for (Atom a : variables) {
......@@ -239,7 +217,7 @@ public class PSP2LTL implements ExpressionVisitor {
* @return the set of booleanAtoms in the compare expression formula.
*/
private List<Atom> getAtoms(String varName, Float threshold, CompareExpression.Operator operator) {
TreeMap<Float, Atom[]> treeMap = rangeMap.get(varName);
TreeMap<Float, Atom[]> treeMap = spec.getRangeMap().get(varName);
if(treeMap == null) {
throw new RuntimeException("Variable " + varName + " not found");
}
......@@ -261,25 +239,5 @@ public class PSP2LTL implements ExpressionVisitor {
}
return vars;
}
/**
* Gets the equal atom.
*
* @param varName the var name
* @param threshold the threshold
* @return the equal atom
*/
private Atom getEqualAtom(String varName, Float threshold) {
return rangeMap.get(varName).get(threshold)[1];
}
/**
* Gets the lower atom.
*
* @param varName the var name
* @param threshold the threshold
* @return the lower atom
*/
public Atom getLowerAtom(String varName, Float threshold) {
return rangeMap.get(varName).get(threshold)[0];
}
}
package it.sagelab.specpro.testing;
import it.sagelab.specpro.models.ltl.LTLDcSpec;
import it.sagelab.specpro.models.ltl.assign.Assignment;
import it.sagelab.specpro.models.ltl.assign.NumericAssignment;
import it.sagelab.specpro.testing.generators.TestGenerator;
import it.sagelab.specpro.testing.oracles.TestOracle;
import it.sagelab.specpro.models.ltl.assign.Trace;
......@@ -15,6 +17,7 @@ public class TestingEnvironment {
private final SUT sut;
private int maxTraceLength;
private boolean stopIfError;
private LTLDcSpec spec;
public TestingEnvironment(TestGenerator testGenerator, TestOracle oracle, SUT sut) {
this.testGenerator = testGenerator;
......@@ -48,6 +51,10 @@ public class TestingEnvironment {
this.maxTraceLength = maxTraceLength;
}
public void enableLTLDcTranslation(LTLDcSpec spec) {
this.spec = spec;
}
public HashMap<Trace, TestOracle.Value> runTests() {
return runTests(null);
}
......@@ -70,13 +77,8 @@ public class TestingEnvironment {
try {
for (Assignment i : input) {
currentInput = i;
Assignment o = sut.exec(i);
trace.add(i.combine(o));
if(trace.last() == null) {
throw new RuntimeException(trace.toString());
}
Assignment t = exec(i);
trace.add(t);
if (trace.size() >= maxTraceLength) {
break;
}
......@@ -113,5 +115,23 @@ public class TestingEnvironment {
return results;
}
private Assignment exec(Assignment i) {
Assignment o;
if(spec != null) {
NumericAssignment numericInput = spec.fromBool2Numeric(i);
o = sut.exec(numericInput);
if(o instanceof NumericAssignment) {
o = spec.fromNumeric2Bool((NumericAssignment) o);
}
} else {
o = sut.exec(i);
}
Assignment c = i.combine(o);
if(c == null) {
throw new RuntimeException("Output " + o + " not compatible with input " + i);
}
return c;
}
}
#Tue Jan 07 15:22:22 CET 2020
build=345
#Tue Jan 21 17:38:32 CET 2020
build=347
version=0.4.0
snapshot=True
package it.sagelab.specpro.fe;
import it.sagelab.specpro.models.InputRequirement;
import it.sagelab.specpro.models.ltl.LTLDcSpec;
import it.sagelab.specpro.models.ltl.LTLSpec;
import it.sagelab.specpro.models.psp.Requirement;
import it.sagelab.specpro.models.psp.Scope;
......@@ -9,6 +10,7 @@ import it.sagelab.specpro.models.psp.qualitative.QualitativeRequirement;
import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Test;
import java.util.Arrays;
import java.util.Collections;
import static org.junit.jupiter.api.Assertions.*;
......@@ -92,6 +94,12 @@ public class PSPFrontEndTests {
assertEquals("(!(_lower_Y0) | !(_equal_Y0))", spec.getInvariants().get(1).toString());
assertEquals("([](!((!(_lower_X0) & !(_equal_X0)))) | <>(((!(_lower_X0) & !(_equal_X0)) & <>((_lower_Y0 & Z)))))",
spec.getRequirements().get(0).toString());
assertTrue(spec instanceof LTLDcSpec);
LTLDcSpec dcSpec = (LTLDcSpec) spec;
assertEquals(2, dcSpec.getNumericVariableNames().size());
assertEquals(1, dcSpec.getThresholds("X").size());
assertEquals(1, dcSpec.getThresholds("Y").size());
}
@Test
......@@ -129,6 +137,12 @@ public class PSPFrontEndTests {
" & <>(((((_lower_X0 | _equal_X0) | _lower_X2) | _equal_X2) | _lower_X1))) -> " +
"((!(!(_equal_X2)) | Z) U ((((_lower_X0 | _equal_X0) | _lower_X2) | _equal_X2) | _lower_X1))))",
spec.getRequirements().get(0).toString());
assertTrue(spec instanceof LTLDcSpec);
LTLDcSpec dcSpec = (LTLDcSpec) spec;
assertEquals(1, dcSpec.getNumericVariableNames().size());
assertEquals(3, dcSpec.getThresholds("X").size());
assertEquals(Arrays.asList(0.0f, 5.0f, 10.0f), dcSpec.getThresholds("X"));
}
......
package it.sagelab.specpro.models.ltl;
import it.sagelab.specpro.models.ltl.assign.Assignment;
import it.sagelab.specpro.models.psp.Scope;
import it.sagelab.specpro.models.psp.expressions.CompareExpression;
import it.sagelab.specpro.models.psp.expressions.NumberExpression;
import it.sagelab.specpro.models.psp.expressions.VariableExpression;
import it.sagelab.specpro.models.psp.qualitative.ExistenceRequirement;
import it.sagelab.specpro.models.psp.qualitative.ResponseRequirement;
import org.junit.jupiter.api.Test;
import java.util.Arrays;
import java.util.Collections;
import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertTrue;
public class LTLDcSpecTests {
@Test
public void testsLTLDcSpecInitialization() {
VariableExpression x = new VariableExpression("X", VariableExpression.Type.FLOAT);
VariableExpression y = new VariableExpression("Y", VariableExpression.Type.FLOAT);
CompareExpression c1 = new CompareExpression(x, new NumberExpression(0f), CompareExpression.Operator.GREATER);
CompareExpression c2 = new CompareExpression(x, new NumberExpression(5.0f), CompareExpression.Operator.EQUAL);
CompareExpression c3 = new CompareExpression(x, new NumberExpression(10.f), CompareExpression.Operator.LOWER_EQUAL);
CompareExpression c4 = new CompareExpression(new NumberExpression(2.0f), y, CompareExpression.Operator.LOWER);
Scope afterC1= new Scope(Scope.Type.AFTER, Arrays.asList(c1));
Scope globally = new Scope(Scope.Type.GLOBALLY, Collections.emptyList());
ResponseRequirement req1 = new ResponseRequirement(afterC1, Arrays.asList(c2, c4));
ExistenceRequirement req2 = new ExistenceRequirement(globally, c3);
LTLDcSpec spec = new LTLDcSpec(Arrays.asList(req1, req2));
assertEquals(2, spec.getNumericVariableNames().size());
assertTrue(spec.getNumericVariableNames().contains("X"));
assertTrue(spec.getNumericVariableNames().contains("Y"));
assertEquals(Arrays.asList(0.0f, 5.0f, 10.f), spec.getThresholds("X"));
assertEquals(Arrays.asList(2.f), spec.getThresholds("Y"));
}
@Test
public void testNumber2BoolAssignment() {
VariableExpression x = new VariableExpression("X", VariableExpression.Type.FLOAT);
VariableExpression y = new VariableExpression("Y", VariableExpression.Type.FLOAT);
CompareExpression c1 = new CompareExpression(x, new NumberExpression(0f), CompareExpression.Operator.GREATER);
CompareExpression c2 = new CompareExpression(x, new NumberExpression(5.0f), CompareExpression.Operator.EQUAL);
CompareExpression c3 = new CompareExpression(x, new NumberExpression(10.f), CompareExpression.Operator.LOWER_EQUAL);
CompareExpression c4 = new CompareExpression(new NumberExpression(2.0f), y, CompareExpression.Operator.LOWER);
Scope afterC1= new Scope(Scope.Type.AFTER, Arrays.asList(c1));
Scope globally = new Scope(Scope.Type.GLOBALLY, Collections.emptyList());
ResponseRequirement req1 = new ResponseRequirement(afterC1, Arrays.asList(c2, c4));
ExistenceRequirement req2 = new ExistenceRequirement(globally, c3);
LTLDcSpec spec = new LTLDcSpec(Arrays.asList(req1, req2));
Assignment ass1 = spec.getDcAssignment("X", 2.f);
assertEquals(false, ass1.getValue(spec.getLowerAtom("X", 0f)));
assertEquals(false, ass1.getValue(spec.getEqualAtom("X", 0f)));
assertEquals(true, ass1.getValue(spec.getLowerAtom("X", 5.0f)));
assertEquals(false, ass1.getValue(spec.getEqualAtom("X", 5.0f)));
assertEquals(false, ass1.getValue(spec.getLowerAtom("X", 10f)));
assertEquals(false, ass1.getValue(spec.getEqualAtom("X", 10f)));
Assignment ass2 = spec.getDcAssignment("X", -10.f);
assertEquals(true, ass2.getValue(spec.getLowerAtom("X", 0f)));
assertEquals(false, ass2.getValue(spec.getEqualAtom("X", 0f)));
assertEquals(false, ass2.getValue(spec.getLowerAtom("X", 5.0f)));
assertEquals(false, ass2.getValue(spec.getEqualAtom("X", 5.0f)));
assertEquals(false, ass2.getValue(spec.getLowerAtom("X", 10f)));
assertEquals(false, ass2.getValue(spec.getEqualAtom("X", 10f)));
Assignment ass3 = spec.getDcAssignment("X", 10.f);
assertEquals(false, ass3.getValue(spec.getLowerAtom("X", 0f)));
assertEquals(false, ass3.getValue(spec.getEqualAtom("X", 0f)));
assertEquals(false, ass3.getValue(spec.getLowerAtom("X", 5.0f)));
assertEquals(false, ass3.getValue(spec.getEqualAtom("X", 5.0f)));
assertEquals(false, ass3.getValue(spec.getLowerAtom("X", 10f)));
assertEquals(true, ass3.getValue(spec.getEqualAtom("X", 10f)));
Assignment ass4 = spec.getDcAssignment("X", 10.1f);
assertEquals(false, ass4.getValue(spec.getLowerAtom("X", 0f)));
assertEquals(false, ass4.getValue(spec.getEqualAtom("X", 0f)));
assertEquals(false, ass4.getValue(spec.getLowerAtom("X", 5.0f)));
assertEquals(false, ass4.getValue(spec.getEqualAtom("X", 5.0f)));
assertEquals(false, ass4.getValue(spec.getLowerAtom("X", 10f)));
assertEquals(false, ass4.getValue(spec.getEqualAtom("X", 10f)));
}
}
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