From 0b63f9b8c3808319c0afe2ada1f87838c7194ff5 Mon Sep 17 00:00:00 2001 From: Masaki Waga Date: Thu, 4 Apr 2024 22:00:34 +0900 Subject: [PATCH] Implemented LTL --- core/src/main/antlr4/AbstractTemporalLogic.g4 | 4 +- core/src/main/antlr4/LTL.g4 | 25 +++ core/src/main/antlr4/STL.g4 | 5 +- .../maswag/AbstractAdaptiveSTLUpdater.java | 18 +- .../net/maswag/AbstractTemporalLogic.java | 45 ++++ .../main/java/net/maswag/AdaptiveSTLList.java | 208 +++++++++--------- .../java/net/maswag/AdaptiveSTLUpdater.java | 6 +- .../java/net/maswag/BlackBoxVerifier.java | 8 +- core/src/main/java/net/maswag/IOSignal.java | 56 +++-- .../main/java/net/maswag/IOSignalPiece.java | 21 +- core/src/main/java/net/maswag/LTLAtomic.java | 56 +++++ core/src/main/java/net/maswag/LTLFactory.java | 26 +++ .../main/java/net/maswag/LTLVisitorImpl.java | 147 +++++++++++++ .../net/maswag/NumericMembershipOracle.java | 2 +- .../maswag/NumericMembershipOracleCost.java | 13 +- core/src/main/java/net/maswag/NumericSUL.java | 2 +- .../java/net/maswag/NumericSULMapper.java | 6 +- .../java/net/maswag/NumericSULVerifier.java | 21 +- core/src/main/java/net/maswag/RoSI.java | 2 +- .../java/net/maswag/STLAbstractAtomic.java | 3 +- core/src/main/java/net/maswag/STLAnd.java | 73 ------ core/src/main/java/net/maswag/STLCost.java | 88 -------- core/src/main/java/net/maswag/STLFactory.java | 6 +- .../main/java/net/maswag/STLInputAtomic.java | 6 +- .../main/java/net/maswag/STLOutputAtomic.java | 4 +- .../main/java/net/maswag/STLVisitorImpl.java | 30 ++- .../main/java/net/maswag/SignalMapper.java | 12 +- .../net/maswag/SignalMapperVisitorImpl.java | 7 +- .../main/java/net/maswag/StaticSTLList.java | 6 +- .../net/maswag/StopDisprovedEQOracle.java | 8 +- .../src/main/java/net/maswag/TemporalAnd.java | 92 ++++++++ ...ventually.java => TemporalEventually.java} | 33 ++- .../{STLGlobal.java => TemporalGlobally.java} | 37 +++- .../{STLImply.java => TemporalImply.java} | 28 ++- .../main/java/net/maswag/TemporalLogic.java | 46 ++++ .../{STLNext.java => TemporalNext.java} | 37 ++-- .../{STLTemporalOp.java => TemporalOp.java} | 14 +- .../maswag/{STLOr.java => TemporalOr.java} | 38 ++-- .../{STLRelease.java => TemporalRelease.java} | 35 ++- .../maswag/{STLSub.java => TemporalSub.java} | 29 ++- .../{STLUntil.java => TemporalUntil.java} | 45 +++- .../java/net/maswag/AdaptiveSTLListTest.java | 20 +- .../java/net/maswag/BlackBoxVerifierTest.java | 7 +- .../test/java/net/maswag/LTLParserTest.java | 81 +++++++ .../java/net/maswag/NumericSULMapperTest.java | 15 +- core/src/test/java/net/maswag/STLAndTest.java | 2 + .../test/java/net/maswag/STLAtomicTest.java | 6 +- .../src/test/java/net/maswag/STLCostTest.java | 39 ++-- .../test/java/net/maswag/STLParserTest.java | 23 +- core/src/test/java/net/maswag/STLSubTest.java | 10 +- .../test/java/net/maswag/STLUntilTest.java | 3 + .../java/net/maswag/SignalMapperTest.java | 16 +- .../java/net/maswag/StaticSTLListTest.java | 5 +- matlab/src/main/java/net/maswag/FalCAuN.java | 14 +- .../java/net/maswag/SimulinkRandomTester.java | 5 +- .../src/main/java/net/maswag/SimulinkSUL.java | 7 +- .../java/net/maswag/AutotransExample.java | 49 ++--- .../maswag/NumericMembershipOracleTest.java | 6 +- .../net/maswag/SimulinkSULMapperTest.java | 7 +- .../test/java/net/maswag/SimulinkSULTest.java | 12 +- .../net/maswag/SimulinkSULVerifierTest.java | 39 ++-- 61 files changed, 1136 insertions(+), 578 deletions(-) create mode 100644 core/src/main/antlr4/LTL.g4 create mode 100644 core/src/main/java/net/maswag/AbstractTemporalLogic.java create mode 100644 core/src/main/java/net/maswag/LTLAtomic.java create mode 100644 core/src/main/java/net/maswag/LTLFactory.java create mode 100644 core/src/main/java/net/maswag/LTLVisitorImpl.java delete mode 100644 core/src/main/java/net/maswag/STLAnd.java delete mode 100644 core/src/main/java/net/maswag/STLCost.java create mode 100644 core/src/main/java/net/maswag/TemporalAnd.java rename core/src/main/java/net/maswag/{STLEventually.java => TemporalEventually.java} (57%) rename core/src/main/java/net/maswag/{STLGlobal.java => TemporalGlobally.java} (57%) rename core/src/main/java/net/maswag/{STLImply.java => TemporalImply.java} (64%) create mode 100644 core/src/main/java/net/maswag/TemporalLogic.java rename core/src/main/java/net/maswag/{STLNext.java => TemporalNext.java} (60%) rename core/src/main/java/net/maswag/{STLTemporalOp.java => TemporalOp.java} (65%) rename core/src/main/java/net/maswag/{STLOr.java => TemporalOr.java} (54%) rename core/src/main/java/net/maswag/{STLRelease.java => TemporalRelease.java} (64%) rename core/src/main/java/net/maswag/{STLSub.java => TemporalSub.java} (75%) rename core/src/main/java/net/maswag/{STLUntil.java => TemporalUntil.java} (58%) create mode 100644 core/src/test/java/net/maswag/LTLParserTest.java diff --git a/core/src/main/antlr4/AbstractTemporalLogic.g4 b/core/src/main/antlr4/AbstractTemporalLogic.g4 index 1ab7d8f4..3a2fd1da 100644 --- a/core/src/main/antlr4/AbstractTemporalLogic.g4 +++ b/core/src/main/antlr4/AbstractTemporalLogic.g4 @@ -51,5 +51,5 @@ MINUS : '-'; FLOAT : NATURAL '.' [0-9]+; LPAREN : '('; RPAREN : ')'; -INPUT : 'input'; -OUTPUT : 'signal' | 'output'; +// This must be the lowest priority token. +ID : [a-zA-Z][a-zA-Z0-9]*; diff --git a/core/src/main/antlr4/LTL.g4 b/core/src/main/antlr4/LTL.g4 new file mode 100644 index 00000000..0e993983 --- /dev/null +++ b/core/src/main/antlr4/LTL.g4 @@ -0,0 +1,25 @@ +grammar LTL; + +@header { +package net.maswag; + +import net.maswag.LTLListener; +import net.maswag.LTLVisitor; +import net.maswag.LTLParser; + +} + +import AbstractTemporalLogic; + +expr + : INPUT EQ ID + | OUTPUT EQ ID + | left=expr binaryOperator right=expr + | unaryOperator expr + | unaryTemporalOperator UNDER interval expr + | left=expr binaryTemporalOperator UNDER interval right=expr + | LPAREN expr RPAREN + ; + +INPUT : 'input'; +OUTPUT : 'output'; diff --git a/core/src/main/antlr4/STL.g4 b/core/src/main/antlr4/STL.g4 index 15f66e02..65fb6e84 100644 --- a/core/src/main/antlr4/STL.g4 +++ b/core/src/main/antlr4/STL.g4 @@ -23,4 +23,7 @@ expr atomic : OUTPUT LPAREN signalID=NATURAL RPAREN comparisonOperator value | INPUT LPAREN signalID=NATURAL RPAREN comparisonOperator value - ; \ No newline at end of file + ; + +INPUT : 'input'; +OUTPUT : 'signal' | 'output'; \ No newline at end of file diff --git a/core/src/main/java/net/maswag/AbstractAdaptiveSTLUpdater.java b/core/src/main/java/net/maswag/AbstractAdaptiveSTLUpdater.java index 160c4a35..cb0d829a 100644 --- a/core/src/main/java/net/maswag/AbstractAdaptiveSTLUpdater.java +++ b/core/src/main/java/net/maswag/AbstractAdaptiveSTLUpdater.java @@ -24,6 +24,8 @@ import java.util.stream.Collectors; import java.util.stream.Stream; +import net.maswag.TemporalLogic.STLCost; + /** * Abstract class for potentially adaptive set of STL formulas * @@ -32,7 +34,7 @@ * @see NumericSULVerifier */ @Slf4j -public abstract class AbstractAdaptiveSTLUpdater implements AdaptiveSTLUpdater { +public abstract class AbstractAdaptiveSTLUpdater implements AdaptiveSTLUpdater { protected static final Function EDGE_PARSER = s -> s; protected EmptinessOracle.MealyEmptinessOracle emptinessOracle; @NotNull @@ -41,11 +43,11 @@ public abstract class AbstractAdaptiveSTLUpdater implements AdaptiveSTLUpdater { protected MembershipOracle.MealyMembershipOracle memOracle; @Setter protected Alphabet inputAlphabet; - private final List STLProperties = new ArrayList<>(); + private final List> STLProperties = new ArrayList<>(); private final List> propertyOracles = new ArrayList<>(); boolean initialized = false; // The list of the STL formulas that are already falsified. - private final List reportedFormulas = new ArrayList<>(); + private final List> reportedFormulas = new ArrayList<>(); public AbstractAdaptiveSTLUpdater() { // Create model checker @@ -53,13 +55,13 @@ public AbstractAdaptiveSTLUpdater() { } @Override - final public List getSTLProperties() { + final public List> getSTLProperties() { return STLProperties; } @Override public List getLTLProperties() { - return this.getSTLProperties().stream().map(STLCost::toLTLString).collect(Collectors.toList()); + return this.getSTLProperties().stream().map(TemporalLogic::toLTLString).collect(Collectors.toList()); } @Override @@ -90,7 +92,7 @@ public void setMemOracle(@NotNull MembershipOracle.MealyMembershipOracle(this.memOracle, multiplier); } - protected void addSTLProperty(STLCost stl) { + protected void addSTLProperty(TemporalLogic stl) { if (STLProperties.contains(stl)) { return; } @@ -102,7 +104,7 @@ protected void addSTLProperty(STLCost stl) { } } - protected void addSTLProperties(Collection stlCollection) { + protected void addSTLProperties(Collection> stlCollection) { stlCollection.forEach(this::addSTLProperty); } @@ -144,7 +146,7 @@ private void confirmInitialization() { } } - public final boolean newlyFalsifiedFormula(STLCost stlFormula) { + public final boolean newlyFalsifiedFormula(TemporalLogic stlFormula) { return !reportedFormulas.contains(stlFormula); } diff --git a/core/src/main/java/net/maswag/AbstractTemporalLogic.java b/core/src/main/java/net/maswag/AbstractTemporalLogic.java new file mode 100644 index 00000000..16db219b --- /dev/null +++ b/core/src/main/java/net/maswag/AbstractTemporalLogic.java @@ -0,0 +1,45 @@ +package net.maswag; + +import lombok.Getter; +import net.automatalib.word.Word; + +import java.util.Set; + +/** + *

Abstract TemporalLogic class.

+ * + * @author Masaki Waga {@literal } + */ +@Getter +public abstract class AbstractTemporalLogic implements TemporalLogic { + boolean nonTemporal; + Set atomicStrings; + + public String toLTLString() { + return this.toAbstractString(); + } + + /** + * {@inheritDoc} + */ + @Override + public Double apply(IOSignal signal) { + return getRoSI(signal).getRobustness(); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + + AbstractTemporalLogic stlCost = (AbstractTemporalLogic) o; + + return this.hashCode() == stlCost.hashCode(); + } + + @Override + public int hashCode() { + // Hash code is implemented based on the string representation. + return this.toString().hashCode(); + } +} diff --git a/core/src/main/java/net/maswag/AdaptiveSTLList.java b/core/src/main/java/net/maswag/AdaptiveSTLList.java index f9595f67..75004578 100644 --- a/core/src/main/java/net/maswag/AdaptiveSTLList.java +++ b/core/src/main/java/net/maswag/AdaptiveSTLList.java @@ -13,17 +13,17 @@ * @see NumericSULVerifier */ @Slf4j -public class AdaptiveSTLList extends AbstractAdaptiveSTLUpdater { - private final List initialSTLs; // list of initial STL formulas - private final List targetSTLs; // list of STL formulas that are targets of falsification - private final List> strengthenedSTLProperties; // list of strengthened STL formulas for each target STL +public class AdaptiveSTLList extends AbstractAdaptiveSTLUpdater { + private final List> initialSTLs; // list of initial STL formulas + private final List> targetSTLs; // list of STL formulas that are targets of falsification + private final List>> strengthenedSTLProperties; // list of strengthened STL formulas for each target STL // list of strengthened STLs generated by statically rewriting operators of each target STL - private final List> candidateSTLProperties; + private final List>> candidateSTLProperties; // list of strengthened STLs generated by adaptively changing intervals of each target STL - private final List> intervalSTLProperties; + private final List>> intervalSTLProperties; // list of STLs that are falsified during BBC - private final List falsifiedSTLProperties; + private final List> falsifiedSTLProperties; // time window of adaptive STL update private final int timeWindow; @@ -31,11 +31,11 @@ public AdaptiveSTLList() { this(Collections.emptySet()); } - public AdaptiveSTLList(STLCost propertyOracle) { + public AdaptiveSTLList(TemporalLogic propertyOracle) { this(Collections.singleton(propertyOracle)); } - public AdaptiveSTLList(Collection STLProperties) { + public AdaptiveSTLList(Collection> STLProperties) { // Use the default duration this(STLProperties, 30); } @@ -44,7 +44,7 @@ public AdaptiveSTLList(Collection STLProperties) { * @param STLProperties The list of STL/LTL formulas to verify * @param timeWindow The maximum time window of the STL formulas. This is typically the number of steps in each simulation. */ - public AdaptiveSTLList(Collection STLProperties, int timeWindow) { + public AdaptiveSTLList(Collection> STLProperties, int timeWindow) { // save original STL formulas to recover when BBC is finished this.initialSTLs = new ArrayList<>(STLProperties); // target STL/LTL formulas to adaptively strengthen @@ -59,7 +59,7 @@ public AdaptiveSTLList(Collection STLProperties, int timeWind // syntactically strengthen targetSTLs this.strengthenedSTLProperties.add(new ArrayList<>()); this.candidateSTLProperties.add(generateStrengthenedSTL(targetSTLs.get(targetIdx))); - if (this.candidateSTLProperties.get(targetIdx).size() > 0) { + if (!this.candidateSTLProperties.get(targetIdx).isEmpty()) { // if there exists any candidate, add one to STLProperties and model-check against it. this.strengthenedSTLProperties.get(targetIdx).add(0, this.candidateSTLProperties.get(targetIdx).remove(0)); } @@ -82,48 +82,48 @@ public AdaptiveSTLList(Collection STLProperties, int timeWind * syntactically strengthen an STL/LTL formula * * @param stl a target STL formula to be strengthen - * @return list of {@link STLCost} objects + * @return list of {@link TemporalLogic} objects */ - private static List strengthenSTL(STLCost stl) { - if (stl instanceof STLOr) { - List subFmls = ((STLOr) stl).getSubFmls(); - List ret = new ArrayList<>(); - ret.add(new STLAnd(subFmls.get(0), subFmls.get(1))); - - strengthenSTL(subFmls.get(0)).forEach(s -> ret.add(new STLOr(s, subFmls.get(1)))); - strengthenSTL(subFmls.get(1)).forEach(s -> ret.add(new STLOr(subFmls.get(0), s))); + private List> strengthenSTL(TemporalLogic stl) { + if (stl instanceof TemporalOr) { + List> subFmls = ((TemporalOr) stl).getSubFmls(); + List> ret = new ArrayList<>(); + ret.add(new TemporalAnd<>(subFmls.get(0), subFmls.get(1))); + + strengthenSTL(subFmls.get(0)).forEach(s -> ret.add(new TemporalOr<>(s, subFmls.get(1)))); + strengthenSTL(subFmls.get(1)).forEach(s -> ret.add(new TemporalOr<>(subFmls.get(0), s))); return ret; } - if (stl instanceof STLAnd) { - List subFmls = ((STLAnd) stl).getSubFormulas(); - List ret = new ArrayList<>(); + if (stl instanceof TemporalAnd) { + List> subFmls = ((TemporalAnd) stl).getSubFormulas(); + List> ret = new ArrayList<>(); - strengthenSTL(subFmls.get(0)).forEach(s -> ret.add(new STLAnd(s, subFmls.get(1)))); - strengthenSTL(subFmls.get(1)).forEach(s -> ret.add(new STLAnd(subFmls.get(0), s))); + strengthenSTL(subFmls.get(0)).forEach(s -> ret.add(new TemporalAnd<>(s, subFmls.get(1)))); + strengthenSTL(subFmls.get(1)).forEach(s -> ret.add(new TemporalAnd<>(subFmls.get(0), s))); return ret; } - if (stl instanceof STLGlobal) { - STLCost subFml = ((STLGlobal) stl).getSubFml(); - List ret = new ArrayList<>(); - strengthenSTL(subFml).forEach(s -> ret.add(new STLGlobal(s))); + if (stl instanceof TemporalGlobally) { + TemporalLogic subFml = ((TemporalGlobally) stl).getSubFml(); + List> ret = new ArrayList<>(); + strengthenSTL(subFml).forEach(s -> ret.add(new TemporalGlobally<>(s))); return ret; } - if (stl instanceof STLUntil) { - STLCost subFmlLeft = ((STLUntil) stl).getLeft(); - STLCost subFmlRight = ((STLUntil) stl).getRight(); + if (stl instanceof TemporalUntil) { + TemporalLogic subFmlLeft = ((TemporalUntil) stl).getLeft(); + TemporalLogic subFmlRight = ((TemporalUntil) stl).getRight(); return new ArrayList<>(Arrays.asList( - new STLAnd(new STLGlobal(subFmlLeft), new STLGlobal(subFmlRight)), - new STLAnd(new STLGlobal(subFmlLeft), new STLEventually(new STLGlobal(subFmlRight))), - new STLAnd(new STLGlobal(subFmlLeft), new STLGlobal(new STLEventually(subFmlRight))) + new TemporalAnd<>(new TemporalGlobally<>(subFmlLeft), new TemporalGlobally<>(subFmlRight)), + new TemporalAnd<>(new TemporalGlobally<>(subFmlLeft), new TemporalEventually<>(new TemporalGlobally<>(subFmlRight))), + new TemporalAnd<>(new TemporalGlobally<>(subFmlLeft), new TemporalGlobally<>(new TemporalEventually<>(subFmlRight))) )); } - if (stl instanceof STLEventually) { - STLCost subFml = ((STLEventually) stl).getSubFml(); + if (stl instanceof TemporalEventually) { + TemporalLogic subFml = ((TemporalEventually) stl).getSubFml(); return new ArrayList<>(Arrays.asList( - new STLGlobal(subFml), - new STLEventually(new STLGlobal(subFml)), - new STLGlobal(new STLEventually(subFml)) + new TemporalGlobally<>(subFml), + new TemporalEventually<>(new TemporalGlobally<>(subFml)), + new TemporalGlobally<>(new TemporalEventually<>(subFml)) )); } return Collections.emptyList(); @@ -139,10 +139,10 @@ private static List strengthenSTL(STLCost stl) { protected void notifyFalsifiedProperty(List falsifiedIndices) { // remove all STL/LTL formula that is falsified from STLProperties falsifiedIndices.sort(Collections.reverseOrder()); - List falsifiedSTLs = new ArrayList<>(); + List> falsifiedSTLs = new ArrayList<>(); List removedIndices = new ArrayList<>(); for (int falsifiedIdx : falsifiedIndices) { - STLCost falsifiedSTL = this.getSTLProperties().get(falsifiedIdx); + TemporalLogic falsifiedSTL = this.getSTLProperties().get(falsifiedIdx); // We remove the STL formula only if it is not an initial formula. if (!initialSTLs.contains(falsifiedSTL)) { removedIndices.add(falsifiedIdx); @@ -154,7 +154,7 @@ protected void notifyFalsifiedProperty(List falsifiedIndices) { // if any targetSTL is falsified, remove all strengthened properties generated from the STL falsifiedIndices.sort(Collections.reverseOrder()); - for (STLCost falsifiedSTL : falsifiedSTLs) { + for (TemporalLogic falsifiedSTL : falsifiedSTLs) { boolean isTarget = false; for (int targetIdx = this.targetSTLs.size() - 1; targetIdx >= 0; targetIdx--) { if (falsifiedSTL.equals(targetSTLs.get(targetIdx))) { @@ -180,7 +180,7 @@ protected void notifyFalsifiedProperty(List falsifiedIndices) { this.strengthenedSTLProperties.get(targetIdx).remove(pos); if (pos < this.intervalSTLProperties.get(targetIdx).size()) { // if the falsified formula is generated by changing intervals, change intervals to make it stronger - STLCost next = this.intervalSTLProperties.get(targetIdx).get(pos).nextStrengthenedSTL(); + TemporalLogic next = this.intervalSTLProperties.get(targetIdx).get(pos).nextStrengthenedSTL(); if (Objects.isNull(next)) { this.intervalSTLProperties.get(targetIdx).remove(pos); } else { @@ -190,7 +190,7 @@ protected void notifyFalsifiedProperty(List falsifiedIndices) { } else { // pick a next STL/LTL formula from candidateSTLProperties if (this.candidateSTLProperties.get(targetIdx).size() > 0) { - STLCost newSTL = nextStrengthenedSTL(targetIdx); + TemporalLogic newSTL = nextStrengthenedSTL(targetIdx); this.strengthenedSTLProperties.get(targetIdx).add(pos, newSTL); log.debug("Adaptive STLProperty(other) is added: " + newSTL.toString()); } @@ -212,7 +212,7 @@ protected void notifyFalsifiedProperty(List falsifiedIndices) { * @param targetStl a target STL/LTL formula * @return list of strengthened formulas */ - private List generateStrengthenedSTL(STLCost targetStl) { + private List> generateStrengthenedSTL(TemporalLogic targetStl) { return strengthenSTL(targetStl); } @@ -222,7 +222,7 @@ private List generateStrengthenedSTL(STLCost targetStl) { * @param targetSTL a target STL/LTL formula * @return list of */ - private List initializeIntervalSTLproperties(STLCost targetSTL) { + private List> initializeIntervalSTLproperties(TemporalLogic targetSTL) { return findIntervalSTL(targetSTL, (s) -> s); } @@ -231,54 +231,54 @@ private List initializeIntervalSTLproperties(STLCost targetSTL) { * * @param stl target STL formula * @param frame outer frame of param 'stl' - * @return list of {@link IntervalSTL} object + * @return list of {@link IntervalTL} object */ - private List findIntervalSTL(STLCost stl, Function frame) { + private List> findIntervalSTL(TemporalLogic stl, Function, TemporalLogic> frame) { // search STLSub and STLNext recursively - if (stl instanceof STLOr) { - List subFmls = ((STLOr) stl).getSubFmls(); - List ret = new ArrayList<>(); + if (stl instanceof TemporalOr) { + List> subFmls = ((TemporalOr) stl).getSubFmls(); + List> ret = new ArrayList<>(); - ret.addAll(findIntervalSTL(subFmls.get(0), (s) -> frame.apply(new STLOr(s, subFmls.get(1))))); - ret.addAll(findIntervalSTL(subFmls.get(1), (s) -> frame.apply(new STLOr(subFmls.get(0), s)))); + ret.addAll(findIntervalSTL(subFmls.get(0), (s) -> frame.apply(new TemporalOr<>(s, subFmls.get(1))))); + ret.addAll(findIntervalSTL(subFmls.get(1), (s) -> frame.apply(new TemporalOr<>(subFmls.get(0), s)))); return ret; } - if (stl instanceof STLAnd) { - List subFmls = ((STLAnd) stl).getSubFormulas(); - List ret = new ArrayList<>(); + if (stl instanceof TemporalAnd) { + List> subFmls = ((TemporalAnd) stl).getSubFormulas(); + List> ret = new ArrayList<>(); - ret.addAll(findIntervalSTL(subFmls.get(0), (s) -> frame.apply(new STLAnd(s, subFmls.get(1))))); - ret.addAll(findIntervalSTL(subFmls.get(1), (s) -> frame.apply(new STLAnd(subFmls.get(0), s)))); + ret.addAll(findIntervalSTL(subFmls.get(0), (s) -> frame.apply(new TemporalAnd<>(s, subFmls.get(1))))); + ret.addAll(findIntervalSTL(subFmls.get(1), (s) -> frame.apply(new TemporalAnd<>(subFmls.get(0), s)))); return ret; } - if (stl instanceof STLGlobal) { - STLCost subFml = ((STLGlobal) stl).getSubFml(); - List ret = new ArrayList<>(); - ret.addAll(findIntervalSTL(subFml, (s) -> frame.apply(new STLGlobal(s)))); + if (stl instanceof TemporalGlobally) { + TemporalLogic subFml = ((TemporalGlobally) stl).getSubFml(); + List> ret = new ArrayList<>(); + ret.addAll(findIntervalSTL(subFml, (s) -> frame.apply(new TemporalGlobally<>(s)))); return ret; } - if (stl instanceof STLSub) { - STLCost subFml = ((STLSub) stl).getSubFml(); - List ret = new ArrayList<>(); - ret.add(new IntervalSTL((STLSub) stl, frame, timeWindow)); + if (stl instanceof TemporalSub) { + TemporalLogic subFml = ((TemporalSub) stl).getSubFml(); + List> ret = new ArrayList<>(); + ret.add(new IntervalTL<>((TemporalSub) stl, frame, timeWindow)); return ret; } - if (stl instanceof STLNext) { - STLCost subFml = ((STLNext) stl).getSubFml(); - List ret = new ArrayList<>(); - ret.add(new IntervalSTL(new STLSub(new STLGlobal(subFml), 1, 1), frame, timeWindow)); + if (stl instanceof TemporalNext) { + TemporalLogic subFml = ((TemporalNext) stl).getSubFml(); + List> ret = new ArrayList<>(); + ret.add(new IntervalTL<>(new TemporalSub<>(new TemporalGlobally<>(subFml), 1, 1), frame, timeWindow)); return ret; } return new ArrayList<>(); } - private STLCost nextStrengthenedSTL(int targetIdx) { + private TemporalLogic nextStrengthenedSTL(int targetIdx) { return this.candidateSTLProperties.get(targetIdx).remove(0); } - private static class IntervalSTL { - public STLSub stl; - public Function frame; + private static class IntervalTL { + public TemporalSub stl; + public Function, TemporalLogic> frame; private final int timeWindow; private final boolean isSTLEventually; private boolean isAssignedCurrent = false; @@ -286,28 +286,28 @@ private static class IntervalSTL { private final int defaultFrom, defaultTo; private int currentFrom, currentTo; - public IntervalSTL(STLSub stl, Function frame, int timeWindow) { + public IntervalTL(TemporalSub stl, Function, TemporalLogic> frame, int timeWindow) { this.stl = stl; this.defaultFrom = stl.getFrom(); this.defaultTo = stl.getTo(); this.frame = frame; this.timeWindow = timeWindow; - STLCost subFml = this.stl.getSubFml(); - this.isSTLEventually = subFml instanceof STLEventually; + TemporalLogic subFml = this.stl.getSubFml(); + this.isSTLEventually = subFml instanceof TemporalEventually; } - public STLCost getOriginalSTL() { + public TemporalLogic getOriginalSTL() { return this.frame.apply(stl); } - public STLCost strengthInit() { - STLCost subFml = this.stl.getSubFml(); - if (subFml instanceof STLGlobal) { + public TemporalLogic strengthInit() { + TemporalLogic subFml = this.stl.getSubFml(); + if (subFml instanceof TemporalGlobally) { return this.frame.apply(subFml); - } else if (subFml instanceof STLEventually) { - STLCost subFml2 = ((STLEventually) subFml).getSubFml(); - return this.frame.apply(new STLGlobal(subFml2)); + } else if (subFml instanceof TemporalEventually) { + TemporalLogic subFml2 = ((TemporalEventually) subFml).getSubFml(); + return this.frame.apply(new TemporalGlobally<>(subFml2)); } // TODO: implement Until return null; @@ -318,21 +318,21 @@ public STLCost strengthInit() { * * @return a strengthened STL formula */ - public STLCost nextStrengthenedSTL() { + public TemporalLogic nextStrengthenedSTL() { if (!isAssignedCurrent) { isAssignedCurrent = true; this.currentFrom = 0; this.currentTo = this.timeWindow / 2; - STLTemporalOp subFml = this.stl.getSubFml(); - if (subFml instanceof STLGlobal) { + TemporalOp subFml = this.stl.getSubFml(); + if (subFml instanceof TemporalGlobally) { this.currentFrom = this.defaultFrom * 3 / 4; this.currentTo = this.defaultTo + ((this.timeWindow - this.defaultTo) / 2); - return this.frame.apply(new STLSub(subFml, currentFrom, currentTo)); - } else if (subFml instanceof STLEventually) { + return this.frame.apply(new TemporalSub<>(subFml, currentFrom, currentTo)); + } else if (subFml instanceof TemporalEventually) { this.currentFrom = this.defaultFrom / 2; this.currentTo = this.defaultFrom + ((this.timeWindow - this.defaultFrom) / 2); - STLCost subFml2 = ((STLEventually) subFml).getSubFml(); - return this.frame.apply(new STLSub(new STLGlobal(subFml2), currentFrom, currentTo)); + TemporalLogic subFml2 = ((TemporalEventually) subFml).getSubFml(); + return this.frame.apply(new TemporalSub<>(new TemporalGlobally<>(subFml2), currentFrom, currentTo)); } return null; } @@ -349,9 +349,9 @@ public STLCost nextStrengthenedSTL() { } this.currentTo = this.defaultTo - ((this.defaultTo - this.currentTo) / 2); } - STLTemporalOp subFml = this.stl.getSubFml(); - if (subFml instanceof STLEventually) { - return this.frame.apply(new STLSub(subFml, currentFrom, currentTo)); + TemporalOp subFml = this.stl.getSubFml(); + if (subFml instanceof TemporalEventually) { + return this.frame.apply(new TemporalSub<>(subFml, currentFrom, currentTo)); } } else { // when changing the interval of Globally operator @@ -367,8 +367,8 @@ public STLCost nextStrengthenedSTL() { this.isEventuallyInterval = true; this.currentFrom = this.defaultFrom; this.currentTo = this.defaultFrom; - STLEventually subFml = (STLEventually) this.stl.getSubFml(); - return this.frame.apply(new STLSub(subFml, defaultFrom, defaultFrom)); + TemporalEventually subFml = (TemporalEventually) this.stl.getSubFml(); + return this.frame.apply(new TemporalSub<>(subFml, defaultFrom, defaultFrom)); } this.currentTo = this.defaultFrom + ((this.currentTo - this.defaultFrom) / 2); } else { @@ -382,12 +382,12 @@ public STLCost nextStrengthenedSTL() { } } - STLTemporalOp subFml = this.stl.getSubFml(); - if (subFml instanceof STLGlobal) { - return this.frame.apply(new STLSub(subFml, currentFrom, currentTo)); - } else if (subFml instanceof STLEventually) { - STLCost subFml2 = ((STLEventually) subFml).getSubFml(); - return this.frame.apply(new STLSub(new STLGlobal(subFml2), currentFrom, currentTo)); + TemporalOp subFml = this.stl.getSubFml(); + if (subFml instanceof TemporalGlobally) { + return this.frame.apply(new TemporalSub<>(subFml, currentFrom, currentTo)); + } else if (subFml instanceof TemporalEventually) { + TemporalLogic subFml2 = ((TemporalEventually) subFml).getSubFml(); + return this.frame.apply(new TemporalSub<>(new TemporalGlobally<>(subFml2), currentFrom, currentTo)); } } return null; @@ -406,7 +406,7 @@ public boolean allDisproved() { public void reset() { List nonInitialIndices = new ArrayList<>(); for (int i = 0; i < size(); i++) { - STLCost stl = this.getSTLProperties().get(i); + TemporalLogic stl = this.getSTLProperties().get(i); if (!initialSTLs.contains(stl)) { nonInitialIndices.add(i); } diff --git a/core/src/main/java/net/maswag/AdaptiveSTLUpdater.java b/core/src/main/java/net/maswag/AdaptiveSTLUpdater.java index c7fbdbf5..645a9a8c 100644 --- a/core/src/main/java/net/maswag/AdaptiveSTLUpdater.java +++ b/core/src/main/java/net/maswag/AdaptiveSTLUpdater.java @@ -17,12 +17,12 @@ * @see BlackBoxVerifier * @see NumericSULVerifier */ -public interface AdaptiveSTLUpdater extends InclusionOracle.MealyInclusionOracle, BlackBoxOracle.MealyBlackBoxOracle { +public interface AdaptiveSTLUpdater extends InclusionOracle.MealyInclusionOracle, BlackBoxOracle.MealyBlackBoxOracle { /** * Returns the current list of STL formulas * The result may change only after the call of findCounterExample */ - List getSTLProperties(); + List> getSTLProperties(); /** * Returns the current list of LTL formulas in the string representation @@ -64,5 +64,5 @@ public interface AdaptiveSTLUpdater extends InclusionOracle.MealyInclusionOracle /** * Returns if the formula is not yet falsified */ - boolean newlyFalsifiedFormula(STLCost stlFormula); + boolean newlyFalsifiedFormula(TemporalLogic stlFormula); } diff --git a/core/src/main/java/net/maswag/BlackBoxVerifier.java b/core/src/main/java/net/maswag/BlackBoxVerifier.java index 27f22120..1c40d34d 100644 --- a/core/src/main/java/net/maswag/BlackBoxVerifier.java +++ b/core/src/main/java/net/maswag/BlackBoxVerifier.java @@ -31,7 +31,7 @@ * * @author Masaki Waga {@literal } */ -class BlackBoxVerifier { +class BlackBoxVerifier { private static final Function EDGE_PARSER = s -> s; final private double multiplier = 1.0; @Getter @@ -43,11 +43,11 @@ class BlackBoxVerifier { private final LearningAlgorithm.MealyLearner learner; private final MealyEQOracleChain eqOracle; @Getter - private final AdaptiveSTLUpdater properties; + private final AdaptiveSTLUpdater properties; @Getter private List> cexInput; @Getter - private List cexProperty; + private List> cexProperty; @Getter private List> cexOutput; private final ModelChecker.MealyModelChecker> modelChecker; @@ -196,7 +196,7 @@ private boolean processMealy() { cexInput = new ArrayList<>(); cexOutput = new ArrayList<>(); boolean isVerified = true; - for (STLCost stlProperty : properties.getSTLProperties()) { + for (TemporalLogic stlProperty : properties.getSTLProperties()) { String ltlProperty = stlProperty.toLTLString(); final MealyMachine cexMealyCandidate = diff --git a/core/src/main/java/net/maswag/IOSignal.java b/core/src/main/java/net/maswag/IOSignal.java index 35f9b7e7..b44146c2 100644 --- a/core/src/main/java/net/maswag/IOSignal.java +++ b/core/src/main/java/net/maswag/IOSignal.java @@ -8,10 +8,10 @@ import java.util.stream.Stream; @Getter -public class IOSignal { - Word> inputSignal, outputSignal; +public class IOSignal { + Word inputSignal, outputSignal; - public IOSignal(Word> inputSignal, Word> outputSignal) { + public IOSignal(Word inputSignal, Word outputSignal) { assert (inputSignal.size() == outputSignal.size()); this.inputSignal = inputSignal; this.outputSignal = outputSignal; @@ -25,49 +25,61 @@ public int length() { return size(); } - public Stream stream() { + public Stream> stream() { return Streams.zip(inputSignal.stream(), outputSignal.stream(), IOSignalPiece::new); } - public List prefixes(boolean longestFirst) { - Queue>> inputSiffixes = new LinkedList<>(inputSignal.prefixes(longestFirst)); - Queue>> outputSiffixes = new LinkedList<>(outputSignal.prefixes(longestFirst)); - List result = new ArrayList<>(); + public List> prefixes(boolean longestFirst) { + Queue> inputSiffixes = new LinkedList<>(inputSignal.prefixes(longestFirst)); + Queue> outputSiffixes = new LinkedList<>(outputSignal.prefixes(longestFirst)); + List> result = new ArrayList<>(); while (!inputSiffixes.isEmpty()) { - result.add(new IOSignal(inputSiffixes.poll(), Objects.requireNonNull(outputSiffixes.poll()))); + result.add(new IOSignal<>(inputSiffixes.poll(), Objects.requireNonNull(outputSiffixes.poll()))); } return result; } - public List suffixes(boolean longestFirst) { - Queue>> inputSiffixes = new LinkedList<>(inputSignal.suffixes(longestFirst)); - Queue>> outputSiffixes = new LinkedList<>(outputSignal.suffixes(longestFirst)); - List result = new ArrayList<>(); + public List> suffixes(boolean longestFirst) { + Queue> inputSuffixes = new LinkedList<>(inputSignal.suffixes(longestFirst)); + Queue> outputSuffixes = new LinkedList<>(outputSignal.suffixes(longestFirst)); + List> result = new ArrayList<>(); - while (!inputSiffixes.isEmpty()) { - result.add(new IOSignal(inputSiffixes.poll(), Objects.requireNonNull(outputSiffixes.poll()))); + while (!inputSuffixes.isEmpty()) { + result.add(new IOSignal<>(inputSuffixes.poll(), Objects.requireNonNull(outputSuffixes.poll()))); } return result; } - public IOSignal suffix(int suffixLen) { - return new IOSignal(inputSignal.suffix(suffixLen), outputSignal.suffix(suffixLen)); + public IOSignal suffix(int suffixLen) { + return new IOSignal<>(inputSignal.suffix(suffixLen), outputSignal.suffix(suffixLen)); } - public IOSignal subWord(int fromIndex) { - return new IOSignal(inputSignal.subWord(fromIndex), outputSignal.subWord(fromIndex)); + public IOSignal subWord(int fromIndex) { + return new IOSignal<>(inputSignal.subWord(fromIndex), outputSignal.subWord(fromIndex)); } - public IOSignal subWord(int fromIndex, int toIndex) { - return new IOSignal(inputSignal.subWord(fromIndex, toIndex), outputSignal.subWord(fromIndex, toIndex)); + public IOSignal subWord(int fromIndex, int toIndex) { + return new IOSignal<>(inputSignal.subWord(fromIndex, toIndex), outputSignal.subWord(fromIndex, toIndex)); } public boolean isEmpty() { return size() == 0; } - public List getOutputSymbol(int i) { + public I getOutputSymbol(int i) { return outputSignal.getSymbol(i); } + + class NumericIOSignal extends IOSignal> { + public NumericIOSignal(Word> inputSignal, Word> outputSignal) { + super(inputSignal, outputSignal); + } + } + + class LogicalIOSignal extends IOSignal> { + public LogicalIOSignal(Word> inputSignal, Word> outputSignal) { + super(inputSignal, outputSignal); + } + } } diff --git a/core/src/main/java/net/maswag/IOSignalPiece.java b/core/src/main/java/net/maswag/IOSignalPiece.java index b5b60df2..f9033add 100644 --- a/core/src/main/java/net/maswag/IOSignalPiece.java +++ b/core/src/main/java/net/maswag/IOSignalPiece.java @@ -1,15 +1,24 @@ package net.maswag; +import lombok.AllArgsConstructor; import lombok.Getter; import java.util.List; +import java.util.Set; -@Getter -public class IOSignalPiece { - final private List inputSignal, outputSignal; +@Getter @AllArgsConstructor +public class IOSignalPiece { + final private I inputSignal, outputSignal; - public IOSignalPiece(List inputSignal, List outputSignal) { - this.inputSignal = inputSignal; - this.outputSignal = outputSignal; + class NumericIOSignalPiece extends IOSignalPiece> { + public NumericIOSignalPiece(List inputSignal, List outputSignal) { + super(inputSignal, outputSignal); + } + } + + class LogicalIOSignalPiece extends IOSignalPiece> { + public LogicalIOSignalPiece(Set inputSignal, Set outputSignal) { + super(inputSignal, outputSignal); + } } } diff --git a/core/src/main/java/net/maswag/LTLAtomic.java b/core/src/main/java/net/maswag/LTLAtomic.java new file mode 100644 index 00000000..e84f6992 --- /dev/null +++ b/core/src/main/java/net/maswag/LTLAtomic.java @@ -0,0 +1,56 @@ +package net.maswag; + +import lombok.AllArgsConstructor; +import net.automatalib.word.Word; + +import java.util.*; +import java.util.stream.Collectors; + +import net.maswag.TemporalLogic.LTLFormula; + +/** + * The atomic propositions in LTL formulas + */ +@AllArgsConstructor +public class LTLAtomic extends AbstractTemporalLogic implements LTLFormula { + private final Optional inputString, outputString; + + @Override + public Set getAllAPs() { + Set result = new HashSet<>(); + result.add(inputString.orElse(outputString.orElse(""))); + result.add(outputString.orElse(inputString.orElse(""))); + return result; + } + + @Override + public void constructAtomicStrings() {} + + @Override + public String toAbstractString() { + List result = new ArrayList<>(); + inputString.ifPresent(s -> result.add("input == " + s + ")")); + outputString.ifPresent(s -> result.add("output == " + s + ")")); + return String.join(" && ", result); + } + + @Override + public String toString() { + List result = new ArrayList<>(); + inputString.ifPresent(s -> result.add("(input == " + s + ")")); + outputString.ifPresent(s -> result.add("(output == " + s + ")")); + return String.join(" && ", result); + } + + @Override + public RoSI getRoSI(IOSignal signal) { + if (signal.isEmpty()) { + return new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY); + } else if (inputString.isPresent() && ! inputString.get().equals(signal.getInputSignal().getSymbol(0)) || + outputString.isPresent() && ! outputString.get().equals(signal.getOutputSignal().getSymbol(0))) { + return new RoSI(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY); + } else { + return new RoSI(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY); + } + } +} diff --git a/core/src/main/java/net/maswag/LTLFactory.java b/core/src/main/java/net/maswag/LTLFactory.java new file mode 100644 index 00000000..26e7b3bc --- /dev/null +++ b/core/src/main/java/net/maswag/LTLFactory.java @@ -0,0 +1,26 @@ +package net.maswag; + +import net.maswag.TemporalLogic.LTLFormula; +import net.maswag.TemporalLogic.STLCost; +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; +import org.antlr.v4.runtime.tree.ParseTree; + +public class LTLFactory { + /** + *

parse an LTL formula

+ * + * @param formula a {@link String} object. + * @return a {@link STLCost} object. + */ + public LTLFormula parse(String formula) { + LTLVisitor visitor = new LTLVisitorImpl(); + CharStream stream = CharStreams.fromString(formula); + LTLLexer lexer = new LTLLexer(stream); + CommonTokenStream tokens = new CommonTokenStream(lexer); + LTLParser parser = new LTLParser(tokens); + ParseTree tree = parser.expr(); + return visitor.visit(tree); + } +} diff --git a/core/src/main/java/net/maswag/LTLVisitorImpl.java b/core/src/main/java/net/maswag/LTLVisitorImpl.java new file mode 100644 index 00000000..58038b25 --- /dev/null +++ b/core/src/main/java/net/maswag/LTLVisitorImpl.java @@ -0,0 +1,147 @@ +package net.maswag; + +import lombok.AllArgsConstructor; +import lombok.NoArgsConstructor; +import lombok.extern.slf4j.Slf4j; +import net.maswag.TemporalAnd.LTLAnd; +import net.maswag.TemporalEventually.LTLEventually; +import net.maswag.TemporalGlobally.LTLGlobally; +import net.maswag.TemporalImply.LTLImply; +import net.maswag.TemporalLogic.LTLFormula; +import net.maswag.TemporalNext.LTLNext; +import net.maswag.TemporalOr.LTLOr; +import net.maswag.TemporalRelease.LTLRelease; +import net.maswag.TemporalSub.LTLSub; +import net.maswag.TemporalUntil.LTLUntil; + +import java.util.List; +import java.util.Map; +import java.util.Optional; + +/** + *

LTLVisitorImpl class.

+ * + * @author Masaki Waga {@literal } + */ +@Slf4j +@NoArgsConstructor +@AllArgsConstructor +public class LTLVisitorImpl extends LTLBaseVisitor { + private List> inputMapper; + private List> outputMapper; + private List largest; + + private LTLFormula handleInterval(TemporalOp subFml, LTLParser.IntervalContext ctx) { + log.trace("Bounded Globally or Eventually"); + int from = Integer.parseInt(ctx.left.getText()); + int to = Integer.parseInt(ctx.right.getText()); + return new LTLSub(subFml, from, to); + } + + /** + * {@inheritDoc} + */ + @Override + public LTLFormula visitExpr(LTLParser.ExprContext ctx) { + if (ctx.INPUT() != null) { + // atomic + log.trace("atomic input"); + return new LTLAtomic(Optional.of(ctx.ID().getText()), Optional.empty()); + } else if (ctx.OUTPUT() != null) { + // atomic + log.trace("atomic output"); + return new LTLAtomic(Optional.empty(), Optional.of(ctx.ID().getText())); + } else if (ctx.binaryOperator() != null) { + // Binary operators without interval + LTLFormula left = visitExpr(ctx.left); + LTLFormula right = visitExpr(ctx.right); + if (ctx.binaryOperator().OR() != null) { + log.trace("or"); + return new LTLOr(left, right); + } else if (ctx.binaryOperator().AND() != null) { + log.trace("and"); + return new LTLAnd(left, right); + } else if (ctx.binaryOperator().IMPLY() != null) { + log.trace("imply"); + return new LTLImply(left, right); + } else if (ctx.binaryOperator().binaryTemporalOperator().UNTIL() != null) { + log.trace("until"); + return new LTLUntil(left, right); + } else if (ctx.binaryOperator().binaryTemporalOperator().RELEASE() != null) { + log.trace("release"); + return new LTLRelease(left, right); + } else { + log.error("Unimplemented formula!!"); + throw new UnsupportedOperationException("Unimplemented formula"); + } + } else if (ctx.unaryOperator() != null) { + // Unary operators without interval + assert ctx.expr().size() == 1; + LTLFormula expr = visitExpr(ctx.expr(0)); + if (ctx.unaryOperator().NEXT() != null) { + log.trace("next"); + return new LTLNext(expr, true); + } else if (ctx.unaryOperator().unaryTemporalOperator().GLOBALLY() != null) { + log.trace("Globally"); + return new LTLGlobally(expr); + } else if (ctx.unaryOperator().unaryTemporalOperator().EVENTUALLY() != null) { + log.trace("Eventually"); + return new LTLEventually(expr); + } else { + log.error("Unimplemented formula!!"); + throw new UnsupportedOperationException("Unimplemented formula"); + } + } else if (ctx.unaryTemporalOperator() != null) { + // Unary operators with interval + assert ctx.expr().size() == 1; + LTLFormula expr = visitExpr(ctx.expr(0)); + if (ctx.unaryTemporalOperator().GLOBALLY() != null) { + log.trace("Globally"); + LTLGlobally global = new LTLGlobally(expr); + + return handleInterval(global, ctx.interval()); + } else if (ctx.unaryTemporalOperator().EVENTUALLY() != null) { + log.trace("Eventually"); + LTLEventually eventually = new LTLEventually(visitExpr(ctx.expr(0))); + + return handleInterval(eventually, ctx.interval()); + } + } else if (ctx.binaryTemporalOperator() != null) { + // Binary operators with interval + LTLFormula left = visitExpr(ctx.left); + LTLFormula right = visitExpr(ctx.right); + if (ctx.binaryTemporalOperator().UNTIL() != null) { + log.trace("Until"); + LTLUntil until = new LTLUntil(left, right); + + if (ctx.interval() != null) { + log.error("Bounded until is not implemented yet"); + return null; + } else { + return until; + } + } else if (ctx.binaryTemporalOperator().RELEASE() != null) { + log.trace("Release"); + LTLRelease release = new LTLRelease(left, right); + + if (ctx.interval() != null) { + log.error("Bounded release is not implemented yet"); + return null; + } else { + return release; + } + } else { + log.error("Unimplemented formula!!"); + throw new UnsupportedOperationException("Unimplemented formula"); + } + } else if (ctx.LPAREN() != null) { + // Paren + log.trace("paren"); + assert ctx.expr().size() == 1; + return visitExpr(ctx.expr(0)); + } + + log.error("Unimplemented formula!!"); + return null; + } +} diff --git a/core/src/main/java/net/maswag/NumericMembershipOracle.java b/core/src/main/java/net/maswag/NumericMembershipOracle.java index f9589486..660621e7 100644 --- a/core/src/main/java/net/maswag/NumericMembershipOracle.java +++ b/core/src/main/java/net/maswag/NumericMembershipOracle.java @@ -61,7 +61,7 @@ public void processQueries(Collection>> que } assert concreteOutput.size() == concreteInput.size(); abstractOutputBuilder.append( - new IOSignal(concreteInput, concreteOutput).stream().map(mapper::mapOutput).collect(Collectors.toList())); + new IOSignal<>(concreteInput, concreteOutput).stream().map(mapper::mapOutput).collect(Collectors.toList())); assert concreteOutput.size() == abstractOutputBuilder.toWord().size(); cache.insert(abstractInput, abstractOutputBuilder.toWord()); diff --git a/core/src/main/java/net/maswag/NumericMembershipOracleCost.java b/core/src/main/java/net/maswag/NumericMembershipOracleCost.java index 51192f38..0ab4536e 100644 --- a/core/src/main/java/net/maswag/NumericMembershipOracleCost.java +++ b/core/src/main/java/net/maswag/NumericMembershipOracleCost.java @@ -10,17 +10,18 @@ import org.slf4j.LoggerFactory; import java.util.*; +import java.util.function.Function; import java.util.stream.Collectors; class NumericMembershipOracleCost extends NumericMembershipOracle implements EvaluationCountable { private static final Logger LOGGER = LoggerFactory.getLogger(NumericMembershipOracleCost.class); private IncrementalMealyBuilder costCache; - private STLCost costFunc; + private Function>, Double> costFunc; private Set notifiedSet = new HashSet<>(); @Getter private int evaluateCount = 0; - NumericMembershipOracleCost(NumericSUL sul, NumericSULMapper mapper, STLCost costFunc) { + NumericMembershipOracleCost(NumericSUL sul, NumericSULMapper mapper, Function>, Double> costFunc) { super(sul, mapper); this.costFunc = costFunc; this.costCache = new IncrementalMealyTreeBuilder<>(mapper.constructAbstractAlphabet()); @@ -65,9 +66,9 @@ Double processQueryWithCost(Query> q) { return null; } assert concreteOutput.size() == concreteInput.size(); - IOSignal concreteSignal = new IOSignal(concreteInput, concreteOutput); + IOSignal> concreteSignal = new IOSignal<>(concreteInput, concreteOutput); List robustness = concreteSignal.prefixes(false).stream() - .map(word -> new IOSignal(word.getInputSignal(), + .map(word -> new IOSignal<>(word.getInputSignal(), Word.fromList(word.stream().map(mapper::mapConcrete).collect(Collectors.toList())))) .map(costFunc).collect(Collectors.toList()) .subList(1, concreteInput.length() + 1); // remove the additional element by prefixes @@ -103,10 +104,10 @@ Double processQueryWithCost(Query> q) { return costBuilder.toWord().lastSymbol(); } - private void cacheInsert(Word abstractInput, IOSignal concreteSignal, Word abstractOutput) { + private void cacheInsert(Word abstractInput, IOSignal> concreteSignal, Word abstractOutput) { super.cacheInsert(abstractInput, abstractOutput); Word robustness = Word.fromList(concreteSignal.prefixes(false).stream() - .map(word -> new IOSignal(word.getInputSignal(), + .map(word -> new IOSignal<>(word.getInputSignal(), Word.fromList(word.stream().map(mapper::mapConcrete).collect(Collectors.toList())))) .map(costFunc).collect(Collectors.toList()) .subList(1, abstractInput.length() + 1)); // remove the additional element by prefixes diff --git a/core/src/main/java/net/maswag/NumericSUL.java b/core/src/main/java/net/maswag/NumericSUL.java index d8fb4239..9ff25980 100644 --- a/core/src/main/java/net/maswag/NumericSUL.java +++ b/core/src/main/java/net/maswag/NumericSUL.java @@ -11,7 +11,7 @@ * * @author Masaki Waga {@literal } */ -public interface NumericSUL extends SUL, IOSignalPiece>, AutoCloseable { +public interface NumericSUL extends SUL, IOSignalPiece>>, AutoCloseable { /** * Execute the SUL by feeding the entire input */ diff --git a/core/src/main/java/net/maswag/NumericSULMapper.java b/core/src/main/java/net/maswag/NumericSULMapper.java index 00ec5bad..b63410c8 100644 --- a/core/src/main/java/net/maswag/NumericSULMapper.java +++ b/core/src/main/java/net/maswag/NumericSULMapper.java @@ -18,7 +18,7 @@ * @author Masaki Waga {@literal } */ @Slf4j -public class NumericSULMapper implements SULMapper, IOSignalPiece> { +public class NumericSULMapper implements SULMapper, IOSignalPiece>> { private Map> inputMapper; private List largestOutputs; private SignalMapper sigMap; @@ -98,7 +98,7 @@ List>> mapInputs(List> abstractInputs) { * {@inheritDoc} */ @Override - public String mapOutput(IOSignalPiece concreteIO) { + public String mapOutput(IOSignalPiece> concreteIO) { List concreteOutput = concreteIO.getOutputSignal(); // System.out.println("AF: " + concreteOutput.get(0)); StringBuilder result = new StringBuilder(concreteOutputs.size()); @@ -122,7 +122,7 @@ public String mapOutput(IOSignalPiece concreteIO) { return result.toString(); } - public List mapConcrete(IOSignalPiece concreteIO) { + public List mapConcrete(IOSignalPiece> concreteIO) { List concreteOutput = concreteIO.getOutputSignal(); List result = new ArrayList<>(concreteOutput); for (int i = 0; i < sigMap.size(); i++) { diff --git a/core/src/main/java/net/maswag/NumericSULVerifier.java b/core/src/main/java/net/maswag/NumericSULVerifier.java index 94a5e52c..72c70bc2 100644 --- a/core/src/main/java/net/maswag/NumericSULVerifier.java +++ b/core/src/main/java/net/maswag/NumericSULVerifier.java @@ -12,6 +12,7 @@ import java.util.*; import java.util.function.Function; +import net.maswag.TemporalLogic.STLCost; import static de.learnlib.filter.cache.sul.SULCaches.createTreeCache; /** @@ -20,10 +21,10 @@ * @author Masaki Waga {@literal } */ public class NumericSULVerifier { - protected SUL, IOSignalPiece> simulink; + protected SUL, IOSignalPiece>> simulink; protected final NumericSUL rawSUL; private final NumericSULMapper mapper; - private final BlackBoxVerifier verifier; + private final BlackBoxVerifier> verifier; private final NumericMembershipOracle memOracle; private final List memOracleCosts = new ArrayList<>(); private final EvaluationCountable.Sum evaluationCountables = new EvaluationCountable.Sum(); @@ -38,7 +39,7 @@ public class NumericSULVerifier { * @param mapper The I/O mapepr between abstract/concrete Simulink models. * @throws java.lang.Exception It can be thrown from the constructor of SimulinkSUL. */ - public NumericSULVerifier(NumericSUL rawSUL, double signalStep, AdaptiveSTLUpdater properties, NumericSULMapper mapper) throws Exception { + public NumericSULVerifier(NumericSUL rawSUL, double signalStep, AdaptiveSTLUpdater> properties, NumericSULMapper mapper) throws Exception { this.rawSUL = rawSUL; this.signalStep = signalStep; this.mapper = mapper; @@ -58,11 +59,11 @@ public NumericSULVerifier(NumericSUL rawSUL, double signalStep, AdaptiveSTLUpdat /** * Returns the falsified STL formulas in the string representation. */ - List getCexProperty() { + List>> getCexProperty() { return verifier.getCexProperty(); } - void addSimulinkEqOracle(STLCost costFunc, + void addSimulinkEqOracle(Function>, Double> costFunc, Function> constructor) { // Define the cost function from a discrete input signal to a double using the Simulink model and the STL formula @@ -127,7 +128,7 @@ void addHillClimbingEQOracle(STLCost costFunc, * @param resetWord a boolean. * @param ltlOracle a {@link de.learnlib.oracle.PropertyOracle.MealyPropertyOracle} object. */ - public void addHillClimbingEQOracle(STLCost costFunc, + public void addHillClimbingEQOracle(Function>, Double> costFunc, int length, Random random, int maxTests, @@ -165,7 +166,7 @@ public void addHillClimbingEQOracleAll(int length, * @param alpha a double. * @param ltlOracle a {@link de.learnlib.oracle.PropertyOracle.MealyPropertyOracle} object. */ - public void addSAEQOracle(STLCost costFunc, + public void addSAEQOracle(Function>, Double> costFunc, int length, Random random, int maxTests, @@ -178,7 +179,7 @@ public void addSAEQOracle(STLCost costFunc, new SAEQOracle(oracle, length, random, maxTests, generationSize, childrenSize, resetWord, alpha, ltlOracle)); } - void addMutateSelectEQOracle(STLCost costFunc, + void addMutateSelectEQOracle(Function>, Double> costFunc, int length, Random random, int maxTests, @@ -202,7 +203,7 @@ void addMutateSelectEQOracle(STLCost costFunc, * @param mutationProbability probability to have mutation * @param ltlOracle the LTL formula */ - void addGAEQOracle(STLCost costFunc, + void addGAEQOracle(Function>, Double> costFunc, int length, int maxTests, ArgParser.GASelectionKind selectionKind, @@ -301,7 +302,7 @@ public int getSimulinkCountForEqTest() { return evaluationCountables.getEvaluateCount(); } - public AdaptiveSTLUpdater getProperties() { + public AdaptiveSTLUpdater> getProperties() { return this.verifier.getProperties(); } diff --git a/core/src/main/java/net/maswag/RoSI.java b/core/src/main/java/net/maswag/RoSI.java index cc7a2240..586c2448 100644 --- a/core/src/main/java/net/maswag/RoSI.java +++ b/core/src/main/java/net/maswag/RoSI.java @@ -3,7 +3,7 @@ import lombok.extern.slf4j.Slf4j; @Slf4j -class RoSI { +public class RoSI { Double lowerBound; Double upperBound; diff --git a/core/src/main/java/net/maswag/STLAbstractAtomic.java b/core/src/main/java/net/maswag/STLAbstractAtomic.java index e881d6e2..a6d9011e 100644 --- a/core/src/main/java/net/maswag/STLAbstractAtomic.java +++ b/core/src/main/java/net/maswag/STLAbstractAtomic.java @@ -6,13 +6,14 @@ import java.util.stream.Collectors; import static java.lang.Math.abs; +import net.maswag.TemporalLogic.STLCost; /** *

STLAtomic class.

* * @author Masaki Waga {@literal } */ -abstract public class STLAbstractAtomic extends STLCost { +abstract public class STLAbstractAtomic extends AbstractTemporalLogic> implements STLCost { protected Operation op; protected int sigIndex; protected double comparator; diff --git a/core/src/main/java/net/maswag/STLAnd.java b/core/src/main/java/net/maswag/STLAnd.java deleted file mode 100644 index 2acaf13a..00000000 --- a/core/src/main/java/net/maswag/STLAnd.java +++ /dev/null @@ -1,73 +0,0 @@ -package net.maswag; - -import lombok.Getter; - -import java.util.*; -import java.util.stream.Collectors; - -@Getter -class STLAnd extends STLCost { - private final List subFormulas; - - STLAnd(STLCost subFml1, STLCost subFml2) { - this.subFormulas = Arrays.asList(subFml1, subFml2); - this.nonTemporal = subFml1.nonTemporal && subFml2.nonTemporal; - } - - STLAnd(List subFormulas) { - this.subFormulas = subFormulas; - this.nonTemporal = subFormulas.stream().map(STLCost::isNonTemporal).reduce((a, b) -> a && b).orElse(false); - } - - - /** - * {@inheritDoc} - */ - @Override - public RoSI getRoSI(IOSignal signal) { - return subFormulas.stream().map(subFml -> subFml.getRoSI(signal)).filter( - Objects::nonNull).reduce(new RoSI(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY), RoSI::min); - } - - /** - * {@inheritDoc} - */ - @Override - public String toString() { - return subFormulas.stream().map(STLCost::toString).collect(Collectors.joining(" && ")); - } - - /** - * {@inheritDoc} - */ - @Override - protected void constructAtomicStrings() { - if (this.nonTemporal) { - this.atomicStrings = new HashSet<>(getAllAPs()); - for (STLCost subFml : subFormulas) { - this.atomicStrings.retainAll(subFml.getAtomicStrings()); - } - } else { - this.atomicStrings = null; - } - } - - /** {@inheritDoc} */ - @Override - protected Set getAllAPs() { - return subFormulas.get(0).getAllAPs(); - } - - /** {@inheritDoc} */ - @Override - public String toAbstractString() { - if (nonTemporal) { - constructAtomicStrings(); - return this.atomicStrings.stream().map( - s -> "( output == \"" + s + "\" )").collect(Collectors.joining(" || ")); - } else { - return this.subFormulas.stream().map(STLCost::toAbstractString).map( - s -> "( " + s + " )").collect(Collectors.joining(" && ")); - } - } -} diff --git a/core/src/main/java/net/maswag/STLCost.java b/core/src/main/java/net/maswag/STLCost.java deleted file mode 100644 index 3239a532..00000000 --- a/core/src/main/java/net/maswag/STLCost.java +++ /dev/null @@ -1,88 +0,0 @@ -package net.maswag; - -import lombok.Getter; -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.antlr.v4.runtime.CommonTokenStream; -import org.antlr.v4.runtime.tree.ParseTree; - -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.function.Function; - -/** - *

Abstract STLCost class.

- * - * @author Masaki Waga {@literal } - */ -@Getter -public abstract class STLCost implements Function { - boolean nonTemporal; - Set atomicStrings; - - /** - *

getAllAPs.

- * - * @return a {@link java.util.Set} object. - */ - protected abstract Set getAllAPs(); - - /** - *

constructAtomicStrings.

- */ - protected abstract void constructAtomicStrings(); - - /** - *

toAbstractString.

- * - * @return a {@link java.lang.String} object. - */ - public abstract String toAbstractString(); - - public String toLTLString() { - return this.toAbstractString(); - } - - private static STLCost parseSTLImpl(String stlFormula, - net.maswag.STLVisitor visitor) { - CharStream stream = CharStreams.fromString(stlFormula); - net.maswag.STLLexer lexer = new net.maswag.STLLexer(stream); - CommonTokenStream tokens = new CommonTokenStream(lexer); - net.maswag.STLParser parser = new net.maswag.STLParser(tokens); - ParseTree tree = parser.expr(); - return visitor.visit(tree); - } - - /** - * {@inheritDoc} - */ - @Override - public Double apply(IOSignal signal) { - return getRoSI(signal).getRobustness(); - } - - /** - *

getRoSI.

- * - * @param signal a {@link net.automatalib.word.Word} object. - * @return a {@link RoSI} object. - */ - public abstract RoSI getRoSI(IOSignal signal); - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - - STLCost stlCost = (STLCost) o; - - return this.hashCode() == stlCost.hashCode(); - } - - @Override - public int hashCode() { - // Hash code is implemented based on the string representation. - return this.toString().hashCode(); - } -} diff --git a/core/src/main/java/net/maswag/STLFactory.java b/core/src/main/java/net/maswag/STLFactory.java index a296debe..0de10e05 100644 --- a/core/src/main/java/net/maswag/STLFactory.java +++ b/core/src/main/java/net/maswag/STLFactory.java @@ -8,6 +8,8 @@ import java.util.List; import java.util.Map; +import net.maswag.TemporalLogic.STLCost; + public class STLFactory { /** *

parse an STL formula using mappers

@@ -15,7 +17,7 @@ public class STLFactory { * @param stlFormula a {@link java.lang.String} object. * @param outputMapper a {@link java.util.List} object. * @param largest a {@link java.util.List} object. - * @return a {@link net.maswag.STLCost} object. + * @return a {@link net.maswag.TemporalLogic.STLCost} object. */ public STLCost parse(String stlFormula, List> inputMapper, @@ -29,7 +31,7 @@ public STLCost parse(String stlFormula, *

parse an STL formula without setting the mapper

* * @param formula a {@link java.lang.String} object. - * @return a {@link net.maswag.STLCost} object. + * @return a {@link net.maswag.TemporalLogic.STLCost} object. */ public STLCost parse(String formula) { net.maswag.STLVisitor visitor = new STLVisitorImpl(); diff --git a/core/src/main/java/net/maswag/STLInputAtomic.java b/core/src/main/java/net/maswag/STLInputAtomic.java index 5a8a91a8..01b8418b 100644 --- a/core/src/main/java/net/maswag/STLInputAtomic.java +++ b/core/src/main/java/net/maswag/STLInputAtomic.java @@ -13,7 +13,7 @@ public class STLInputAtomic extends STLAbstractAtomic { private final List> abstractInputs = new ArrayList<>(); private final List> concreteInputs = new ArrayList<>(); - private List largest = new ArrayList<>(); + private final List largest = new ArrayList<>(); private List> inputMapper; /** @@ -36,7 +36,7 @@ public Set getAllAPs() { } @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { constructAtomicStrings(concreteInputs, abstractInputs, largest); } @@ -65,7 +65,7 @@ void setInputMapper(List> inputMapper) { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal> signal) { return getRoSISingle(signal.getInputSignal()); } diff --git a/core/src/main/java/net/maswag/STLOutputAtomic.java b/core/src/main/java/net/maswag/STLOutputAtomic.java index ac56f691..71695a5b 100644 --- a/core/src/main/java/net/maswag/STLOutputAtomic.java +++ b/core/src/main/java/net/maswag/STLOutputAtomic.java @@ -36,7 +36,7 @@ public Set getAllAPs() { } @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { constructAtomicStrings(concreteOutputs, abstractOutputs, largest); } @@ -72,7 +72,7 @@ void setLargest(List largest) { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal> signal) { return getRoSISingle(signal.getOutputSignal()); } diff --git a/core/src/main/java/net/maswag/STLVisitorImpl.java b/core/src/main/java/net/maswag/STLVisitorImpl.java index 62ad2ebb..c80831a9 100644 --- a/core/src/main/java/net/maswag/STLVisitorImpl.java +++ b/core/src/main/java/net/maswag/STLVisitorImpl.java @@ -3,6 +3,16 @@ import lombok.AllArgsConstructor; import lombok.NoArgsConstructor; import lombok.extern.slf4j.Slf4j; +import net.maswag.TemporalAnd.STLAnd; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalRelease.STLRelease; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalUntil.STLUntil; import java.util.List; import java.util.Map; @@ -22,16 +32,12 @@ public class STLVisitorImpl extends net.maswag.STLBaseVisitor { private List> outputMapper; private List largest; - private STLCost handleInterval(STLTemporalOp subFml, net.maswag.STLParser.IntervalContext ctx) { - - if (ctx == null) { - return subFml; - } else { - log.trace("Bounded Globally or Eventually"); - int from = Integer.parseInt(ctx.left.getText()); - int to = Integer.parseInt(ctx.right.getText()); - return new STLSub(subFml, from, to); - } + private STLCost handleInterval(TemporalOp> subFml, net.maswag.STLParser.IntervalContext ctx) { + assert (ctx != null); + log.trace("Bounded Globally or Eventually"); + int from = Integer.parseInt(ctx.left.getText()); + int to = Integer.parseInt(ctx.right.getText()); + return new STLSub(subFml, from, to); } /** @@ -75,7 +81,7 @@ public STLCost visitExpr(net.maswag.STLParser.ExprContext ctx) { return new STLNext(expr, true); } else if (ctx.unaryOperator().unaryTemporalOperator().GLOBALLY() != null) { log.trace("Globally"); - return new STLGlobal(expr); + return new STLGlobally(expr); } else if (ctx.unaryOperator().unaryTemporalOperator().EVENTUALLY() != null) { log.trace("Eventually"); return new STLEventually(expr); @@ -89,7 +95,7 @@ public STLCost visitExpr(net.maswag.STLParser.ExprContext ctx) { STLCost expr = visitExpr(ctx.expr(0)); if (ctx.unaryTemporalOperator().GLOBALLY() != null) { log.trace("Globally"); - STLGlobal global = new STLGlobal(expr); + STLGlobally global = new STLGlobally(expr); return handleInterval(global, ctx.interval()); } else if (ctx.unaryTemporalOperator().EVENTUALLY() != null) { diff --git a/core/src/main/java/net/maswag/SignalMapper.java b/core/src/main/java/net/maswag/SignalMapper.java index 52d7e688..05b9b9fe 100644 --- a/core/src/main/java/net/maswag/SignalMapper.java +++ b/core/src/main/java/net/maswag/SignalMapper.java @@ -22,7 +22,7 @@ */ @RequiredArgsConstructor public class SignalMapper { - final private List> sigMap; + final private List>, Double>> sigMap; public SignalMapper() { this.sigMap = Collections.emptyList(); @@ -30,7 +30,7 @@ public SignalMapper() { //@ requires 0 <= index < size() - public double apply(int index, IOSignalPiece concreteSignal) { + public double apply(int index, IOSignalPiece> concreteSignal) { return this.sigMap.get(index).apply(concreteSignal); } @@ -40,18 +40,18 @@ public int size() { } public static SignalMapper parse(String filename) throws IOException { - List> rawList = new BufferedReader( + List>, Double>> rawList = new BufferedReader( new InputStreamReader(new FileInputStream(filename))).lines().map(SignalMapper::lineParse).collect(Collectors.toList()); return new SignalMapper(rawList); } - static Function lineParse(String line) { - net.maswag.SignalMapperVisitor> visitor = new SignalMapperVisitorImpl(); + static Function>, Double> lineParse(String line) { + net.maswag.SignalMapperVisitor>, Double>> visitor = new SignalMapperVisitorImpl(); return parseSignalMapperImpl(line, visitor); } - private static Function parseSignalMapperImpl(String line, net.maswag.SignalMapperVisitor> visitor) { + private static Function>, Double> parseSignalMapperImpl(String line, net.maswag.SignalMapperVisitor>, Double>> visitor) { CharStream stream = CharStreams.fromString(line); net.maswag.SignalMapperLexer lexer = new net.maswag.SignalMapperLexer(stream); CommonTokenStream tokens = new CommonTokenStream(lexer); diff --git a/core/src/main/java/net/maswag/SignalMapperVisitorImpl.java b/core/src/main/java/net/maswag/SignalMapperVisitorImpl.java index 435629d7..567a6182 100644 --- a/core/src/main/java/net/maswag/SignalMapperVisitorImpl.java +++ b/core/src/main/java/net/maswag/SignalMapperVisitorImpl.java @@ -2,6 +2,7 @@ import lombok.extern.slf4j.Slf4j; +import java.util.List; import java.util.Objects; import java.util.function.Function; @@ -13,12 +14,12 @@ * @author Masaki Waga {@literal } */ @Slf4j -public class SignalMapperVisitorImpl extends net.maswag.SignalMapperBaseVisitor> { +public class SignalMapperVisitorImpl extends net.maswag.SignalMapperBaseVisitor>, Double>> { /** * {@inheritDoc} */ @Override - public Function visitExpr(net.maswag.SignalMapperParser.ExprContext ctx) { + public Function>, Double> visitExpr(net.maswag.SignalMapperParser.ExprContext ctx) { if (ctx.atomic() != null) { // atomic log.trace("atomic"); @@ -63,7 +64,7 @@ public Function visitExpr(net.maswag.SignalMapperParser.E * {@inheritDoc} */ @Override - public Function visitAtomic(net.maswag.SignalMapperParser.AtomicContext ctx) { + public Function>, Double> visitAtomic(net.maswag.SignalMapperParser.AtomicContext ctx) { if (ctx.signalID != null) { int sigIndex = Integer.parseInt(ctx.signalID.getText()); if (Objects.nonNull(ctx.INPUT())) { diff --git a/core/src/main/java/net/maswag/StaticSTLList.java b/core/src/main/java/net/maswag/StaticSTLList.java index 6f949eb2..ba194792 100644 --- a/core/src/main/java/net/maswag/StaticSTLList.java +++ b/core/src/main/java/net/maswag/StaticSTLList.java @@ -9,18 +9,18 @@ * @see BlackBoxVerifier * @see NumericSULVerifier */ -public class StaticSTLList extends AbstractAdaptiveSTLUpdater { +public class StaticSTLList extends AbstractAdaptiveSTLUpdater { Set disprovedIndices = new HashSet<>(); public StaticSTLList() { this(Collections.emptySet()); } - public StaticSTLList(STLCost propertyOracle) { + public StaticSTLList(TemporalLogic propertyOracle) { this(Collections.singleton(propertyOracle)); } - public StaticSTLList(Collection STLProperties) { + public StaticSTLList(Collection> STLProperties) { super(); this.addSTLProperties(STLProperties); } diff --git a/core/src/main/java/net/maswag/StopDisprovedEQOracle.java b/core/src/main/java/net/maswag/StopDisprovedEQOracle.java index 96a07051..2521d72f 100644 --- a/core/src/main/java/net/maswag/StopDisprovedEQOracle.java +++ b/core/src/main/java/net/maswag/StopDisprovedEQOracle.java @@ -26,16 +26,16 @@ * @author Masaki Waga {@literal } */ @Slf4j -public class StopDisprovedEQOracle implements EquivalenceOracle.MealyEquivalenceOracle { +public class StopDisprovedEQOracle implements EquivalenceOracle.MealyEquivalenceOracle { - private final AdaptiveSTLUpdater ltlOracles; + private final AdaptiveSTLUpdater ltlOracles; private final MealyEquivalenceOracle eqOracle; /** * @param eqOracle the wrapped equivalence oracle * @param ltlOracles ltlOracles */ - StopDisprovedEQOracle(MealyEquivalenceOracle eqOracle, AdaptiveSTLUpdater ltlOracles) { + StopDisprovedEQOracle(MealyEquivalenceOracle eqOracle, AdaptiveSTLUpdater ltlOracles) { this.eqOracle = eqOracle; this.ltlOracles = ltlOracles; } @@ -60,7 +60,7 @@ public DefaultQuery> findCounterExample(MealyMachine hypo @Slf4j @AllArgsConstructor static - class StaticLTLList extends AbstractAdaptiveSTLUpdater { + class StaticLTLList extends AbstractAdaptiveSTLUpdater { List ltlProperties; Set disprovedIndices = new HashSet<>(); diff --git a/core/src/main/java/net/maswag/TemporalAnd.java b/core/src/main/java/net/maswag/TemporalAnd.java new file mode 100644 index 00000000..1c780018 --- /dev/null +++ b/core/src/main/java/net/maswag/TemporalAnd.java @@ -0,0 +1,92 @@ +package net.maswag; + +import lombok.Getter; + +import java.util.*; +import java.util.stream.Collectors; + +@Getter +class TemporalAnd extends AbstractTemporalLogic { + private final List> subFormulas; + + TemporalAnd(TemporalLogic subFml1, TemporalLogic subFml2) { + this.subFormulas = Arrays.asList(subFml1, subFml2); + this.nonTemporal = subFml1.isNonTemporal() && subFml2.isNonTemporal(); + } + + TemporalAnd(List> subFormulas) { + this.subFormulas = subFormulas; + this.nonTemporal = subFormulas.stream().map(TemporalLogic::isNonTemporal).reduce((a, b) -> a && b).orElse(false); + } + + /** + * {@inheritDoc} + */ + @Override + public RoSI getRoSI(IOSignal signal) { + return subFormulas.stream().map(subFml -> subFml.getRoSI(signal)).filter( + Objects::nonNull).reduce(new RoSI(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY), RoSI::min); + } + + /** + * {@inheritDoc} + */ + @Override + public String toString() { + return subFormulas.stream().map(TemporalLogic::toString).collect(Collectors.joining(" && ")); + } + + /** + * {@inheritDoc} + */ + @Override + public void constructAtomicStrings() { + if (this.nonTemporal) { + this.atomicStrings = new HashSet<>(getAllAPs()); + for (TemporalLogic subFml : subFormulas) { + this.atomicStrings.retainAll(subFml.getAtomicStrings()); + } + } else { + this.atomicStrings = null; + } + } + + /** {@inheritDoc} */ + @Override + public Set getAllAPs() { + return subFormulas.get(0).getAllAPs(); + } + + /** {@inheritDoc} */ + @Override + public String toAbstractString() { + if (nonTemporal) { + constructAtomicStrings(); + return this.atomicStrings.stream().map( + s -> "( output == \"" + s + "\" )").collect(Collectors.joining(" || ")); + } else { + return this.subFormulas.stream().map(TemporalLogic::toAbstractString).map( + s -> "( " + s + " )").collect(Collectors.joining(" && ")); + } + } + + static class STLAnd extends TemporalAnd> implements STLCost { + STLAnd(STLCost subFml1, STLCost subFml2) { + super(subFml1, subFml2); + } + + STLAnd(List>> subFormulas) { + super(subFormulas); + } + } + + static class LTLAnd extends TemporalAnd implements LTLFormula { + LTLAnd(LTLFormula subFml1, LTLFormula subFml2) { + super(subFml1, subFml2); + } + + LTLAnd(List> subFormulas) { + super(subFormulas); + } + } +} diff --git a/core/src/main/java/net/maswag/STLEventually.java b/core/src/main/java/net/maswag/TemporalEventually.java similarity index 57% rename from core/src/main/java/net/maswag/STLEventually.java rename to core/src/main/java/net/maswag/TemporalEventually.java index 76bcf636..13a799a4 100644 --- a/core/src/main/java/net/maswag/STLEventually.java +++ b/core/src/main/java/net/maswag/TemporalEventually.java @@ -1,6 +1,8 @@ package net.maswag; import java.util.Objects; +import java.util.Set; +import java.util.List; /** @@ -8,8 +10,8 @@ * * @author Masaki Waga {@literal } */ -public class STLEventually extends STLTemporalOp { - STLEventually(STLCost subFml) { +public class TemporalEventually extends TemporalOp { + TemporalEventually(TemporalLogic subFml) { super(subFml); } @@ -17,14 +19,14 @@ public class STLEventually extends STLTemporalOp { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { return getRoSIRaw(signal).assignMax(new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY)); } /** * {@inheritDoc} */ - public RoSI getRoSIRaw(IOSignal signal) { + public RoSI getRoSIRaw(IOSignal signal) { return signal.suffixes(true).stream().map(w -> subFml.getRoSI(w)).filter(Objects::nonNull) .reduce(new RoSI(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY), RoSI::max); } @@ -32,7 +34,7 @@ public RoSI getRoSIRaw(IOSignal signal) { /** * {@inheritDoc} */ - public RoSI getRoSIRawWithLen(IOSignal signal, int length) { + public RoSI getRoSIRawWithLen(IOSignal signal, int length) { return signal.suffixes(true).subList(0, length).stream().map(w -> subFml.getRoSI(w)).filter(Objects::nonNull) .reduce(new RoSI(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY), RoSI::max); } @@ -56,8 +58,25 @@ public String toAbstractString() { /** *

getSubFml.

* - * @return a {@link STLCost} object. + * @return a {@link TemporalLogic} object. */ - public STLCost getSubFml() { return this.subFml; } + public TemporalLogic getSubFml() { return this.subFml; } + + static class STLEventually extends TemporalEventually> implements STLCost { + STLEventually(STLCost subFml) { + super(subFml); + } + + @Override + public STLCost getSubFml() { + return (STLCost) this.subFml; + } + } + + static class LTLEventually extends TemporalEventually implements LTLFormula { + LTLEventually(LTLFormula subFml) { + super(subFml); + } + } } diff --git a/core/src/main/java/net/maswag/STLGlobal.java b/core/src/main/java/net/maswag/TemporalGlobally.java similarity index 57% rename from core/src/main/java/net/maswag/STLGlobal.java rename to core/src/main/java/net/maswag/TemporalGlobally.java index e525855e..351f32ac 100644 --- a/core/src/main/java/net/maswag/STLGlobal.java +++ b/core/src/main/java/net/maswag/TemporalGlobally.java @@ -1,14 +1,20 @@ package net.maswag; +import net.automatalib.word.Word; + +import java.util.List; import java.util.Objects; +import java.util.Set; + +import net.maswag.TemporalLogic.*; /** *

STLGlobal class.

* * @author Masaki Waga {@literal } */ -public class STLGlobal extends STLTemporalOp { - STLGlobal(STLCost subFml) { +public class TemporalGlobally extends TemporalOp { + TemporalGlobally(TemporalLogic subFml) { super(subFml); } @@ -16,14 +22,14 @@ public class STLGlobal extends STLTemporalOp { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { return getRoSIRaw(signal).assignMin(new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY)); } /** * {@inheritDoc} */ - public RoSI getRoSIRaw(IOSignal signal) { + public RoSI getRoSIRaw(IOSignal signal) { return signal.suffixes(true).stream().filter(w -> !w.isEmpty()).map(w -> subFml.getRoSI(w)).filter(Objects::nonNull) .reduce(new RoSI(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY), RoSI::min); } @@ -31,7 +37,7 @@ public RoSI getRoSIRaw(IOSignal signal) { /** * {@inheritDoc} */ - public RoSI getRoSIRawWithLen(IOSignal signal, int length) { + public RoSI getRoSIRawWithLen(IOSignal signal, int length) { return signal.suffixes(true).subList(0, length).stream().filter(w -> !w.isEmpty()).map(w -> subFml.getRoSI(w)).filter(Objects::nonNull) .reduce(new RoSI(Double.POSITIVE_INFINITY, Double.POSITIVE_INFINITY), RoSI::min); } @@ -55,7 +61,24 @@ public String toString() { /** *

getSubFml.

* - * @return a {@link STLCost} object. + * @return a {@link TemporalLogic} object. */ - public STLCost getSubFml() { return this.subFml; } + public TemporalLogic getSubFml() { return this.subFml; } + + static class STLGlobally extends TemporalGlobally> implements STLCost { + STLGlobally(STLCost subFml) { + super(subFml); + } + + @Override + public STLCost getSubFml() { + return (STLCost) this.subFml; + } + } + + static class LTLGlobally extends TemporalGlobally implements LTLFormula { + LTLGlobally(LTLFormula subFml) { + super(subFml); + } + } } diff --git a/core/src/main/java/net/maswag/STLImply.java b/core/src/main/java/net/maswag/TemporalImply.java similarity index 64% rename from core/src/main/java/net/maswag/STLImply.java rename to core/src/main/java/net/maswag/TemporalImply.java index 20b95cde..227155b7 100644 --- a/core/src/main/java/net/maswag/STLImply.java +++ b/core/src/main/java/net/maswag/TemporalImply.java @@ -1,6 +1,7 @@ package net.maswag; import java.util.HashSet; +import java.util.List; import java.util.Set; import java.util.stream.Collectors; @@ -9,13 +10,14 @@ * * @author Masaki Waga {@literal } */ -public class STLImply extends STLCost { - private STLCost subFml1, subFml2; +public class TemporalImply extends AbstractTemporalLogic { + private final TemporalLogic subFml1; + private final TemporalLogic subFml2; - STLImply(STLCost subFml1, STLCost subFml2) { + TemporalImply(TemporalLogic subFml1, TemporalLogic subFml2) { this.subFml1 = subFml1; this.subFml2 = subFml2; - this.nonTemporal = subFml1.nonTemporal && subFml2.nonTemporal; + this.nonTemporal = subFml1.isNonTemporal() && subFml2.isNonTemporal(); } @@ -23,7 +25,7 @@ public class STLImply extends STLCost { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { return subFml1.getRoSI(signal).assignNegate().assignMax(subFml2.getRoSI(signal)); } @@ -31,7 +33,7 @@ public RoSI getRoSI(IOSignal signal) { * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { if (this.nonTemporal) { if (this.atomicStrings == null) { this.atomicStrings = new HashSet<>(getAllAPs()); @@ -45,7 +47,7 @@ protected void constructAtomicStrings() { /** {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { return subFml1.getAllAPs(); } @@ -66,5 +68,17 @@ public String toAbstractString() { public String toString() { return String.format("( %s ) -> ( %s )", subFml1.toString(), subFml2.toString()); } + + static class STLImply extends TemporalImply> implements STLCost { + STLImply(STLCost subFml1, STLCost subFml2) { + super(subFml1, subFml2); + } + } + + static class LTLImply extends TemporalImply implements LTLFormula { + LTLImply(LTLFormula subFml1, LTLFormula subFml2) { + super(subFml1, subFml2); + } + } } diff --git a/core/src/main/java/net/maswag/TemporalLogic.java b/core/src/main/java/net/maswag/TemporalLogic.java new file mode 100644 index 00000000..d7d131bc --- /dev/null +++ b/core/src/main/java/net/maswag/TemporalLogic.java @@ -0,0 +1,46 @@ +package net.maswag; + +import lombok.Getter; +import net.automatalib.word.Word; + +import java.util.Collection; +import java.util.List; +import java.util.Set; +import java.util.function.Function; + +/** + *

Abstract TemporalLogic class.

+ * + * @author Masaki Waga {@literal } + */ +public interface TemporalLogic extends Function, Double> { + /** + *

toAbstractString.

+ * + * @return a {@link String} object. + */ + String toAbstractString(); + + String toLTLString(); + + /** + *

getRoSI.

+ * + * @return a {@link RoSI} object. + */ + RoSI getRoSI(IOSignal signal); + + Double apply(IOSignal signal); + + Set getAllAPs(); + + void constructAtomicStrings(); + + boolean isNonTemporal(); + + Collection getAtomicStrings(); + + interface STLCost extends TemporalLogic> {} + + interface LTLFormula extends TemporalLogic {} +} diff --git a/core/src/main/java/net/maswag/STLNext.java b/core/src/main/java/net/maswag/TemporalNext.java similarity index 60% rename from core/src/main/java/net/maswag/STLNext.java rename to core/src/main/java/net/maswag/TemporalNext.java index aadf291d..f3146a67 100644 --- a/core/src/main/java/net/maswag/STLNext.java +++ b/core/src/main/java/net/maswag/TemporalNext.java @@ -1,5 +1,8 @@ package net.maswag; +import lombok.Getter; + +import java.util.List; import java.util.Set; /** @@ -7,11 +10,12 @@ * * @author Masaki Waga {@literal } */ -public class STLNext extends STLCost { - private STLCost subFml; - private boolean nullPositive; +public class TemporalNext extends AbstractTemporalLogic { + @Getter + private TemporalLogic subFml; + private final boolean nullPositive; - STLNext(STLCost subFml, boolean nullPositive) { + TemporalNext(TemporalLogic subFml, boolean nullPositive) { this.subFml = subFml; this.nullPositive = nullPositive; this.nonTemporal = false; @@ -21,7 +25,7 @@ public class STLNext extends STLCost { * {@inheritDoc} */ @Override - public Double apply(IOSignal signal) { + public Double apply(IOSignal signal) { if (signal.size() <= 1) { return this.nullPositive ? Double.POSITIVE_INFINITY : Double.NEGATIVE_INFINITY; } @@ -32,7 +36,7 @@ public Double apply(IOSignal signal) { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { if (signal.size() <= 1) { return new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY); } @@ -43,7 +47,7 @@ public RoSI getRoSI(IOSignal signal) { * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { this.atomicStrings = null; } @@ -57,7 +61,7 @@ public String toAbstractString() { /** {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { return subFml.getAllAPs(); } @@ -67,10 +71,15 @@ public String toString() { return String.format("X ( %s )", subFml.toString()); } - /** - *

getSubFml.

- * - * @return a {@link STLCost} object. - */ - public STLCost getSubFml() { return this.subFml; } + static class STLNext extends TemporalNext> implements STLCost { + STLNext(STLCost subFml, boolean nullPositive) { + super(subFml, nullPositive); + } + } + + static class LTLNext extends TemporalNext implements LTLFormula { + LTLNext(LTLFormula subFml, boolean nullPositive) { + super(subFml, nullPositive); + } + } } diff --git a/core/src/main/java/net/maswag/STLTemporalOp.java b/core/src/main/java/net/maswag/TemporalOp.java similarity index 65% rename from core/src/main/java/net/maswag/STLTemporalOp.java rename to core/src/main/java/net/maswag/TemporalOp.java index 5b2f905c..cd3c1027 100644 --- a/core/src/main/java/net/maswag/STLTemporalOp.java +++ b/core/src/main/java/net/maswag/TemporalOp.java @@ -2,10 +2,10 @@ import java.util.Set; -abstract class STLTemporalOp extends STLCost { - STLCost subFml; +abstract class TemporalOp extends AbstractTemporalLogic { + TemporalLogic subFml; - STLTemporalOp(STLCost subFml) { + TemporalOp(TemporalLogic subFml) { this.subFml = subFml; this.nonTemporal = false; } @@ -16,7 +16,7 @@ abstract class STLTemporalOp extends STLCost { * @param signal a {@link net.automatalib.word.Word} object. * @return a RoSI object. */ - abstract public RoSI getRoSIRaw(IOSignal signal); + abstract public RoSI getRoSIRaw(IOSignal signal); /** *

getRoSIRawLen.

@@ -25,13 +25,13 @@ abstract class STLTemporalOp extends STLCost { * @param length the length to compute the RoSI * @return a RoSI object. */ - abstract public RoSI getRoSIRawWithLen(IOSignal signal, int length); + abstract public RoSI getRoSIRawWithLen(IOSignal signal, int length); /** * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { this.atomicStrings = null; } @@ -39,7 +39,7 @@ protected void constructAtomicStrings() { * {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { return subFml.getAllAPs(); } } diff --git a/core/src/main/java/net/maswag/STLOr.java b/core/src/main/java/net/maswag/TemporalOr.java similarity index 54% rename from core/src/main/java/net/maswag/STLOr.java rename to core/src/main/java/net/maswag/TemporalOr.java index 64269c87..fbbb986e 100644 --- a/core/src/main/java/net/maswag/STLOr.java +++ b/core/src/main/java/net/maswag/TemporalOr.java @@ -8,17 +8,17 @@ * * @author Masaki Waga {@literal } */ -public class STLOr extends STLCost { - private List subFmls; +public class TemporalOr extends AbstractTemporalLogic { + private List> subFmls; - STLOr(STLCost subFml1, STLCost subFml2) { + TemporalOr(TemporalLogic subFml1, TemporalLogic subFml2) { this.subFmls = Arrays.asList(subFml1, subFml2); - this.nonTemporal = subFml1.nonTemporal && subFml2.nonTemporal; + this.nonTemporal = subFml1.isNonTemporal() && subFml2.isNonTemporal(); } - STLOr(List subFmls) { + TemporalOr(List> subFmls) { this.subFmls = subFmls; - this.nonTemporal = subFmls.stream().map(STLCost::isNonTemporal).reduce((a, b) -> a && b).orElse(false); + this.nonTemporal = subFmls.stream().map(TemporalLogic::isNonTemporal).reduce((a, b) -> a && b).orElse(false); } /** @@ -35,17 +35,17 @@ public RoSI getRoSI(IOSignal signal) { */ @Override public String toString() { - return subFmls.stream().map(STLCost::toString).collect(Collectors.joining(" || ")); + return subFmls.stream().map(TemporalLogic::toString).collect(Collectors.joining(" || ")); } /** * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { if (this.nonTemporal) { this.atomicStrings = new HashSet<>(); - for (STLCost subFml : subFmls) { + for (TemporalLogic subFml : subFmls) { this.atomicStrings.addAll(subFml.getAtomicStrings()); } } else { @@ -55,7 +55,7 @@ protected void constructAtomicStrings() { /** {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { return subFmls.get(0).getAllAPs(); } @@ -67,7 +67,7 @@ public String toAbstractString() { return this.atomicStrings.stream().map( s -> "( output == \"" + s + "\" )").collect(Collectors.joining(" || ")); } else { - return this.subFmls.stream().map(STLCost::toAbstractString).map( + return this.subFmls.stream().map(TemporalLogic::toAbstractString).map( s -> "( " + s + " )").collect(Collectors.joining(" || ")); } } @@ -75,7 +75,19 @@ public String toAbstractString() { /** *

getSubFmls.

* - * @return {@link STLCost} list object. + * @return {@link TemporalLogic} list object. */ - public List getSubFmls() { return this.subFmls; } + public List> getSubFmls() { return this.subFmls; } + + static class STLOr extends TemporalOr> implements STLCost { + STLOr(STLCost subFml1, STLCost subFml2) { + super(subFml1, subFml2); + } + } + + static class LTLOr extends TemporalOr implements LTLFormula { + LTLOr(TemporalLogic subFml1, TemporalLogic subFml2) { + super(subFml1, subFml2); + } + } } diff --git a/core/src/main/java/net/maswag/STLRelease.java b/core/src/main/java/net/maswag/TemporalRelease.java similarity index 64% rename from core/src/main/java/net/maswag/STLRelease.java rename to core/src/main/java/net/maswag/TemporalRelease.java index 145c5172..5ac18eb5 100644 --- a/core/src/main/java/net/maswag/STLRelease.java +++ b/core/src/main/java/net/maswag/TemporalRelease.java @@ -1,5 +1,6 @@ package net.maswag; +import java.util.List; import java.util.Objects; import java.util.Set; @@ -8,10 +9,10 @@ * * @author Masaki Waga {@literal } */ -public class STLRelease extends STLCost { - private final STLCost left, right; +public class TemporalRelease extends AbstractTemporalLogic { + private final TemporalLogic left, right; - STLRelease(STLCost left, STLCost right) { + TemporalRelease(TemporalLogic left, TemporalLogic right) { this.left = left; this.right = right; this.nonTemporal = false; @@ -21,11 +22,11 @@ public class STLRelease extends STLCost { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { return getRoSIRaw(signal).assignMax(new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY)); } - public RoSI getRoSIRaw(IOSignal signal) { + public RoSI getRoSIRaw(IOSignal signal) { RoSI result = new RoSI(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY); for (int i = 0; i < signal.length(); i++) { @@ -49,7 +50,7 @@ public String toString() { * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { this.atomicStrings = null; } @@ -58,7 +59,7 @@ protected void constructAtomicStrings() { * {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { Set allAPs = this.left.getAllAPs(); allAPs.addAll(this.right.getAllAPs()); return allAPs; @@ -75,18 +76,30 @@ public String toAbstractString() { /** *

getLeft.

* - * @return a left {@link STLCost} object. + * @return a left {@link TemporalLogic} object. */ - public STLCost getLeft() { + public TemporalLogic getLeft() { return this.left; } /** *

getRight.

* - * @return a right {@link STLCost} object. + * @return a right {@link TemporalLogic} object. */ - public STLCost getRight() { + public TemporalLogic getRight() { return this.right; } + + static class STLRelease extends TemporalRelease> implements STLCost { + STLRelease(STLCost left, STLCost right) { + super(left, right); + } + } + + static class LTLRelease extends TemporalRelease implements LTLFormula { + LTLRelease(LTLFormula left, LTLFormula right) { + super(left, right); + } + } } diff --git a/core/src/main/java/net/maswag/STLSub.java b/core/src/main/java/net/maswag/TemporalSub.java similarity index 75% rename from core/src/main/java/net/maswag/STLSub.java rename to core/src/main/java/net/maswag/TemporalSub.java index b7b295df..e1773d62 100644 --- a/core/src/main/java/net/maswag/STLSub.java +++ b/core/src/main/java/net/maswag/TemporalSub.java @@ -3,12 +3,13 @@ import lombok.extern.slf4j.Slf4j; import java.util.ArrayList; +import java.util.List; import java.util.Set; @Slf4j -public class STLSub extends STLCost { +public class TemporalSub extends AbstractTemporalLogic { - private STLTemporalOp subFml; + private TemporalOp subFml; private int from, to; /** @@ -16,7 +17,7 @@ public class STLSub extends STLCost { * @param from the first index, inclusive * @param to the last index, inclusive. */ - STLSub(STLTemporalOp subFml, int from, int to) { + TemporalSub(TemporalOp subFml, int from, int to) { this.subFml = subFml; this.from = from; this.to = to; @@ -24,7 +25,7 @@ public class STLSub extends STLCost { } @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { if (from >= signal.size()) { // If the signal is too short return new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY); @@ -38,7 +39,7 @@ public RoSI getRoSI(IOSignal signal) { } @Override - protected Set getAllAPs() { + public Set getAllAPs() { return subFml.getAllAPs(); } @@ -52,7 +53,7 @@ public String toString() { } @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { this.atomicStrings = null; } @@ -85,9 +86,9 @@ public String toAbstractString() { /** *

getSubFml.

* - * @return a {@link STLTemporalOp} object. + * @return a {@link TemporalLogic} object. */ - public STLTemporalOp getSubFml() { return this.subFml; } + public TemporalOp getSubFml() { return this.subFml; } /** *

getFrom.

@@ -102,4 +103,16 @@ public String toAbstractString() { * @return a int of 'to'. */ public int getTo() { return this.to; } + + static class STLSub extends TemporalSub> implements STLCost { + STLSub(TemporalOp> subFml, int from, int to) { + super(subFml, from, to); + } + } + + static class LTLSub extends TemporalSub implements LTLFormula { + LTLSub(TemporalOp subFml, int from, int to) { + super(subFml, from, to); + } + } } diff --git a/core/src/main/java/net/maswag/STLUntil.java b/core/src/main/java/net/maswag/TemporalUntil.java similarity index 58% rename from core/src/main/java/net/maswag/STLUntil.java rename to core/src/main/java/net/maswag/TemporalUntil.java index 5c9e2c53..38d5d338 100644 --- a/core/src/main/java/net/maswag/STLUntil.java +++ b/core/src/main/java/net/maswag/TemporalUntil.java @@ -1,5 +1,6 @@ package net.maswag; +import java.util.List; import java.util.Objects; import java.util.Set; @@ -8,10 +9,10 @@ * * @author Masaki Waga {@literal } */ -public class STLUntil extends STLCost { - private STLCost left, right; +public class TemporalUntil extends AbstractTemporalLogic { + private TemporalLogic left, right; - STLUntil(STLCost left, STLCost right) { + TemporalUntil(TemporalLogic left, TemporalLogic right) { this.left = left; this.right = right; this.nonTemporal = false; @@ -21,11 +22,11 @@ public class STLUntil extends STLCost { * {@inheritDoc} */ @Override - public RoSI getRoSI(IOSignal signal) { + public RoSI getRoSI(IOSignal signal) { return getRoSIRaw(signal).assignMax(new RoSI(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY)); } - public RoSI getRoSIRaw(IOSignal signal) { + public RoSI getRoSIRaw(IOSignal signal) { RoSI result = new RoSI(Double.NEGATIVE_INFINITY, Double.NEGATIVE_INFINITY); for (int i = 0; i < signal.length(); i++) { @@ -50,7 +51,7 @@ public String toString() { * {@inheritDoc} */ @Override - protected void constructAtomicStrings() { + public void constructAtomicStrings() { this.atomicStrings = null; } @@ -59,7 +60,7 @@ protected void constructAtomicStrings() { * {@inheritDoc} */ @Override - protected Set getAllAPs() { + public Set getAllAPs() { Set allAPs = this.left.getAllAPs(); allAPs.addAll(this.right.getAllAPs()); return allAPs; @@ -76,14 +77,36 @@ public String toAbstractString() { /** *

getLeft.

* - * @return a left {@link STLCost} object. + * @return a left {@link TemporalLogic} object. */ - public STLCost getLeft() { return this.left; } + public TemporalLogic getLeft() { return this.left; } /** *

getRight.

* - * @return a right {@link STLCost} object. + * @return a right {@link TemporalLogic} object. */ - public STLCost getRight() { return this.right; } + public TemporalLogic getRight() { return this.right; } + + static class STLUntil extends TemporalUntil> implements STLCost { + STLUntil(STLCost left, STLCost right) { + super(left, right); + } + + @Override + public STLCost getLeft() { + return (STLCost) super.getLeft(); + } + + @Override + public STLCost getRight() { + return (STLCost) super.getRight(); + } + } + + static class LTLUntil extends TemporalUntil implements LTLFormula { + LTLUntil(TemporalLogic left, TemporalLogic right) { + super(left, right); + } + } } diff --git a/core/src/test/java/net/maswag/AdaptiveSTLListTest.java b/core/src/test/java/net/maswag/AdaptiveSTLListTest.java index d77b62a4..66fa7250 100644 --- a/core/src/test/java/net/maswag/AdaptiveSTLListTest.java +++ b/core/src/test/java/net/maswag/AdaptiveSTLListTest.java @@ -1,5 +1,6 @@ package net.maswag; +import net.maswag.TemporalLogic.STLCost; import org.junit.jupiter.api.Test; import java.util.ArrayList; @@ -11,17 +12,16 @@ import static org.hamcrest.MatcherAssert.assertThat; import static org.hamcrest.collection.IsIterableContainingInAnyOrder.containsInAnyOrder; import static org.junit.jupiter.api.Assertions.assertEquals; - class AdaptiveSTLListTest { List stlList; - AdaptiveSTLList adaptiveSTLList; + AdaptiveSTLList> adaptiveSTLList; int timeWindow = 30; @Test void strengthenEventually() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("[] (<> output(0) < 1.5)")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = new ArrayList<>(Arrays.asList( factory.parse("[] ([] (output(0) < 1.5))"), @@ -57,7 +57,7 @@ void strengthenEventually() { void strengthenOr() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("(output(0) < 1.5) && ((output(1) > 2.0) || (output(2) < 2.5))")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = new ArrayList<>(Arrays.asList( factory.parse("(output(0) < 1.5) && ((output(1) > 2.0) && (output(2) < 2.5))"), @@ -79,7 +79,7 @@ void strengthenOr() { void strengthenUntil() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("((output(0) < 3.0) U (output(1) > 3.5)) && (output(2) < 4.0)")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = new ArrayList<>(Arrays.asList( factory.parse("(([] (output(0) < 3.0)) && ([] (output(1) > 3.5))) && (output(2) < 4.0)"), factory.parse("((output(0) < 3.0) U (output(1) > 3.5)) && (output(2) < 4.0)") @@ -114,7 +114,7 @@ void strengthenUntil() { void strengthenGlobalInterval() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("([]_[0, 4] (output(0) < 4.5)) && (output(1) > 5.0)")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = new ArrayList<>(Arrays.asList( factory.parse("([] (output(0) < 4.5)) && (output(1) > 5.0)"), @@ -164,7 +164,7 @@ void strengthenGlobalInterval() { void strengthenEventuallyInterval() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("(output(0) < 5.5) && (<>_[2, 10] (output(1) > 6.0))")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = new ArrayList<>(Arrays.asList( factory.parse("(output(0) < 5.5) && ([] (output(1) > 6.0))"), @@ -242,7 +242,7 @@ void strengthenEventuallyInterval() { void strengthenNext() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("(X (output(0) < 6.5)) && (output(1) > 7.0)")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); ArrayList expected = new ArrayList<>(Arrays.asList( factory.parse("([] (output(0) < 6.5)) && (output(1) > 7.0)"), @@ -293,7 +293,7 @@ void strengthenNext() { void strengthenCompoundSTL() { STLFactory factory = new STLFactory(); stlList = Collections.singletonList(factory.parse("([]_[3, 10] (output(1) > 2.2)) && ([] (<> output(2) < 5.1))")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); ArrayList expected = new ArrayList<>(Arrays.asList( factory.parse("([] ( output(1) > 2.200000 )) && [] ( <> ( output(2) < 5.100000 ) )"), factory.parse("([]_[3, 10] ( output(1) > 2.200000 )) && [] ( [] ( output(2) < 5.100000 ) )"), @@ -350,7 +350,7 @@ void strengthenMultipleSTLs() { factory.parse("(output(0) > 2.0) || (output(1) < 2.5)"), factory.parse("(output(0) > 7.0) U (output(1) < 6.6)"), factory.parse("(X (output(0) < 3.5)) && (<> output(1) > 9.0)")); - adaptiveSTLList = new AdaptiveSTLList(stlList, timeWindow); + adaptiveSTLList = new AdaptiveSTLList<>(stlList, timeWindow); List expected = Arrays.asList( factory.parse("(output(0) > 2.0) && (output(1) < 2.5)"), factory.parse("([] output(0) > 7.0) && ([] output(1) < 6.6)"), diff --git a/core/src/test/java/net/maswag/BlackBoxVerifierTest.java b/core/src/test/java/net/maswag/BlackBoxVerifierTest.java index b8f25172..e67f1e76 100644 --- a/core/src/test/java/net/maswag/BlackBoxVerifierTest.java +++ b/core/src/test/java/net/maswag/BlackBoxVerifierTest.java @@ -9,6 +9,10 @@ import net.automatalib.automaton.transducer.CompactMealy; import net.automatalib.util.automaton.builder.AutomatonBuilders; import net.automatalib.word.WordBuilder; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; @@ -18,7 +22,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertFalse; import static org.mockito.Mockito.*; - class BlackBoxVerifierTest { private final Alphabet inputAlphabet = new ArrayAlphabet<>("a"); StaticSTLList stlList; @@ -38,7 +41,7 @@ void setUp() { List properties = Arrays.asList( new STLNext(new STLNext(new STLNext(events.get(1), true), true), true), events.get(0), - new STLGlobal(new STLImply(events.get(1), new STLNext(events.get(0), true))), + new STLGlobally(new STLImply(events.get(1), new STLNext(events.get(0), true))), new STLNext(new STLNext(events.get(1), true), true)); falsifiedProperties = new ArrayList<>(); falsifiedProperties.add(properties.get(3)); diff --git a/core/src/test/java/net/maswag/LTLParserTest.java b/core/src/test/java/net/maswag/LTLParserTest.java new file mode 100644 index 00000000..eecec740 --- /dev/null +++ b/core/src/test/java/net/maswag/LTLParserTest.java @@ -0,0 +1,81 @@ +package net.maswag; + +import net.maswag.TemporalAnd.LTLAnd; +import net.maswag.TemporalEventually.LTLEventually; +import net.maswag.TemporalGlobally.LTLGlobally; +import net.maswag.TemporalImply.LTLImply; +import net.maswag.TemporalLogic.LTLFormula; +import net.maswag.TemporalNext.LTLNext; +import net.maswag.TemporalOr.LTLOr; +import net.maswag.TemporalRelease.LTLRelease; +import net.maswag.TemporalSub.LTLSub; +import net.maswag.TemporalUntil.LTLUntil; +import org.junit.jupiter.api.Test; + +import java.util.Arrays; +import java.util.List; +import java.util.Optional; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +class LTLParserTest { + LTLFactory factory = new LTLFactory(); + + @Test + void atomic() { + List inputs = Arrays.asList( + "input == a", "(input == b)", + "output == p", "output == q"); + List expectedList = Arrays.asList( + new LTLAtomic(Optional.of("a"), Optional.empty()), + new LTLAtomic(Optional.of("b"), Optional.empty()), + new LTLAtomic(Optional.empty(), Optional.of("p")), + new LTLAtomic(Optional.empty(), Optional.of("q"))); + + for (int i = 0; i < inputs.size(); i++) { + LTLFormula result = factory.parse(inputs.get(i)); + + assertEquals(expectedList.get(i).toString(), result.toString()); + } + } + + @Test + void expr() { + List inputs = Arrays.asList( + "input == a", + "output == p", + "input == a || output == p", + "input == a -> output == p", + "input == a && output == p", + "X (input == a)", + "[] (output == p)", + "<> (input == a)", + "alw_[0,2] (output == p)", + "ev_[10,20] (input == a)", + "(input == a) U (output == p)", // Until + "(input == a) R (output == p)" // Release + ); + LTLAtomic left = new LTLAtomic(Optional.of("a"), Optional.empty()); + LTLAtomic right = new LTLAtomic(Optional.empty(), Optional.of("p")); + List expectedList = Arrays.asList( + left, right, + new LTLOr(left, right), + new LTLImply(left, right), + new LTLAnd(left, right), + new LTLNext(left, true), + new LTLGlobally(right), + new LTLEventually(left), + new LTLSub(new LTLGlobally(right), 0, 2), + new LTLSub(new LTLEventually(left), 10, 20), + new LTLUntil(left, right), + new LTLRelease(left, right) + ); + + assert inputs.size() == expectedList.size(); + + for (int i = 0; i < inputs.size(); i++) { + LTLFormula result = factory.parse(inputs.get(i)); + assertEquals(expectedList.get(i).toString(), result.toString()); + } + } +} diff --git a/core/src/test/java/net/maswag/NumericSULMapperTest.java b/core/src/test/java/net/maswag/NumericSULMapperTest.java index 691ad7a5..76d58273 100644 --- a/core/src/test/java/net/maswag/NumericSULMapperTest.java +++ b/core/src/test/java/net/maswag/NumericSULMapperTest.java @@ -8,7 +8,16 @@ import java.util.function.Function; import static org.junit.jupiter.api.Assertions.assertEquals; - +import net.maswag.TemporalAnd.STLAnd; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalRelease.STLRelease; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalUntil.STLUntil; class NumericSULMapperTest { private List> inputMapper; @@ -86,8 +95,8 @@ void setUp() { mapper2.put('c', 100.0); inputMapper = new ArrayList<>(Arrays.asList(mapper1, mapper2)); } - Function diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); - List> sigMap = new ArrayList<>(Collections.singletonList(diff)); + Function>, Double> diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); + List>, Double>> sigMap = new ArrayList<>(Collections.singletonList(diff)); List> outputMapper; List largest; { diff --git a/core/src/test/java/net/maswag/STLAndTest.java b/core/src/test/java/net/maswag/STLAndTest.java index 9477911e..797fe58e 100644 --- a/core/src/test/java/net/maswag/STLAndTest.java +++ b/core/src/test/java/net/maswag/STLAndTest.java @@ -11,6 +11,8 @@ import static java.lang.Math.min; import static org.junit.jupiter.api.Assertions.assertEquals; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalAnd.STLAnd; @RunWith(JUnitQuickcheck.class) public class STLAndTest { diff --git a/core/src/test/java/net/maswag/STLAtomicTest.java b/core/src/test/java/net/maswag/STLAtomicTest.java index da227d88..9aabf281 100644 --- a/core/src/test/java/net/maswag/STLAtomicTest.java +++ b/core/src/test/java/net/maswag/STLAtomicTest.java @@ -2,6 +2,7 @@ import net.automatalib.word.Word; import net.automatalib.word.WordBuilder; +import net.maswag.TemporalLogic.STLCost; import org.junit.jupiter.api.Test; import java.util.ArrayList; @@ -9,12 +10,11 @@ import java.util.List; import static org.junit.jupiter.api.Assertions.assertEquals; - class STLAtomicTest { @Test void applyEmpty() { - IOSignal signal = new IOSignal(Word.epsilon(), Word.epsilon()); + IOSignal> signal = new IOSignal<>(Word.epsilon(), Word.epsilon()); STLCost formula = new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 10); double expected = Double.POSITIVE_INFINITY; double actual = formula.apply(signal); @@ -29,7 +29,7 @@ void ne() { Word> signal = builder.toWord(); STLCost formula = new STLOutputAtomic(0, STLOutputAtomic.Operation.ne, 2); double expected = 2; - double actual = formula.apply(new IOSignal(signal, signal)); + double actual = formula.apply(new IOSignal<>(signal, signal)); assertEquals(expected, actual); } diff --git a/core/src/test/java/net/maswag/STLCostTest.java b/core/src/test/java/net/maswag/STLCostTest.java index 43df958f..58fdf34a 100644 --- a/core/src/test/java/net/maswag/STLCostTest.java +++ b/core/src/test/java/net/maswag/STLCostTest.java @@ -11,6 +11,13 @@ import static java.lang.Double.*; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotEquals; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalEventually.STLEventually; + class STLCostTest { private List concreteExpected; @@ -45,8 +52,8 @@ void setUp() { } formulas = Arrays.asList( - new STLGlobal(atomics.get(0)), - new STLGlobal(new STLImply(atomics.get(1), atomics.get(2))) + new STLGlobally(atomics.get(0)), + new STLGlobally(new STLImply(atomics.get(1), atomics.get(2))) ); assert concreteExpected.size() == formulas.size(); @@ -105,8 +112,8 @@ void setUp() { @Test void ATExampleS4() { STLCost costFunc = - new STLOr(new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 100)), 0, 13), - new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 65.0)), 14, 14)); + new STLOr(new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 100)), 0, 13), + new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 65.0)), 14, 14)); assertNotEquals(POSITIVE_INFINITY, costFunc.apply(input)); } @@ -114,8 +121,8 @@ void ATExampleS4() { void ATExampleS4AndTextRepl() { STLFactory factory = new STLFactory(); STLCost costFuncExt = - new STLOr(new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 100)), 0, 13), - new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 65.0)), 14, 14)); + new STLOr(new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 100)), 0, 13), + new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 65.0)), 14, 14)); STLCost costFunc = factory.parse("([]_[0,13] (signal(0) < 100)) || ([]_[14,14] (signal(0) > 65.0))"); assertEquals(costFuncExt.apply(input), costFunc.apply(input)); } @@ -152,12 +159,12 @@ void setUp() { void AT6() { STLCost costFunc1Atomic = new STLOutputAtomic(1, STLOutputAtomic.Operation.lt, 3000); - STLTemporalOp costFunc1Global = - new STLGlobal(costFunc1Atomic); + TemporalOp> costFunc1Global = + new STLGlobally(costFunc1Atomic); STLCost costFunc1 = new STLSub(costFunc1Global, 0, 15); STLCost costFunc2 = - new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 35.0)), 0, 2); + new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 35.0)), 0, 2); STLCost costFunc = new STLImply(costFunc1, costFunc2); RoSI robustness1Atomic = costFunc1Atomic.getRoSI(input); @@ -185,8 +192,8 @@ void AT6() { void AT6TextRepl() { STLFactory factory = new STLFactory(); STLCost costFuncExt = - new STLImply(new STLSub(new STLGlobal(new STLOutputAtomic(1, STLOutputAtomic.Operation.lt, 3000)), 0, 15), - new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 35.0)), 0, 2)); + new STLImply(new STLSub(new STLGlobally(new STLOutputAtomic(1, STLOutputAtomic.Operation.lt, 3000)), 0, 15), + new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.lt, 35.0)), 0, 2)); STLCost costFunc = factory.parse("((alw_[0, 15] (signal(1) < 3000.0)) -> (alw_[0, 2] (signal(0) < 35.0)))"); assertEquals(costFuncExt.apply(input), costFunc.apply(input)); } @@ -194,7 +201,7 @@ void AT6TextRepl() { @Nested class Bug20210308Test { - IOSignal input; + IOSignal> input; @BeforeEach void setUp() { @@ -216,7 +223,7 @@ void setUp() { builder.append(new ArrayList<>(Arrays.asList(-70.00499399229089, -58.495021874998656, -43.38252812500288, -31.858421875002815, -22.020599999999433))); Word> inputWord = builder.toWord(); inputWord.stream().forEach(line -> line.add(line.get(4) - line.get(3))); - input = new IOSignal(inputWord, inputWord); + input = new IOSignal<>(inputWord, inputWord); assert Objects.requireNonNull(input.getOutputSymbol(0)).size() == 6; } @@ -224,13 +231,13 @@ void setUp() { void CC4() { STLCost costFunc1Atomic = new STLOutputAtomic(5, STLOutputAtomic.Operation.gt, 8); - STLTemporalOp costFunc1Global = - new STLGlobal(costFunc1Atomic); + TemporalOp> costFunc1Global = + new STLGlobally(costFunc1Atomic); STLCost costFunc1 = new STLSub(costFunc1Global, 0, 2); STLCost costFunc2 = new STLSub(new STLEventually(costFunc1), 0, 3); - STLCost costFunc = new STLSub(new STLGlobal(costFunc2), 0, 6); + STLCost costFunc = new STLSub(new STLGlobally(costFunc2), 0, 6); RoSI robustness1Atomic = costFunc1Atomic.getRoSI(input); assertNotEquals(POSITIVE_INFINITY, robustness1Atomic.lowerBound); diff --git a/core/src/test/java/net/maswag/STLParserTest.java b/core/src/test/java/net/maswag/STLParserTest.java index 3ece66fa..58debb34 100644 --- a/core/src/test/java/net/maswag/STLParserTest.java +++ b/core/src/test/java/net/maswag/STLParserTest.java @@ -1,5 +1,15 @@ package net.maswag; +import net.maswag.TemporalAnd.STLAnd; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalRelease.STLRelease; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalUntil.STLUntil; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CommonTokenStream; @@ -15,7 +25,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertThrows; - class STLParserTest { @Test @@ -76,22 +85,22 @@ void setUp() { new STLImply(new STLOutputAtomic(0, lt, -1.0), new STLOutputAtomic(1, eq, 2.2)), new STLNext(new STLOutputAtomic(1, eq, -20), true), - new STLGlobal(new STLOutputAtomic(1, eq, -20)), + new STLGlobally(new STLOutputAtomic(1, eq, -20)), new STLEventually(new STLOutputAtomic(1, eq, -20)), new STLSub( - new STLGlobal(new STLOutputAtomic(1, eq, -20)), 0, 2), + new STLGlobally(new STLOutputAtomic(1, eq, -20)), 0, 2), new STLSub( new STLEventually(new STLOutputAtomic(1, eq, -20)), 10, 20), - new STLGlobal(new STLImply( + new STLGlobally(new STLImply( new STLAnd( new STLOutputAtomic(2, ne, 4.0), new STLNext(new STLOutputAtomic(2, eq, 4.0), false)), - new STLSub(new STLGlobal(new STLOutputAtomic(2, eq, 4.0)), 0, 1))), + new STLSub(new STLGlobally(new STLOutputAtomic(2, eq, 4.0)), 0, 1))), // S2 - new STLGlobal(new STLImply(new STLOutputAtomic(2, STLOutputAtomic.Operation.eq, 3), + new STLGlobally(new STLImply(new STLOutputAtomic(2, STLOutputAtomic.Operation.eq, 3), new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 20))), // S5 - new STLGlobal( + new STLGlobally( new STLOr( new STLOutputAtomic(1, STLOutputAtomic.Operation.lt, 4770), new STLNext(new STLOutputAtomic(1, STLOutputAtomic.Operation.gt, 600.0), true))), diff --git a/core/src/test/java/net/maswag/STLSubTest.java b/core/src/test/java/net/maswag/STLSubTest.java index fd180831..1f4a61a6 100644 --- a/core/src/test/java/net/maswag/STLSubTest.java +++ b/core/src/test/java/net/maswag/STLSubTest.java @@ -1,13 +1,19 @@ package net.maswag; import net.automatalib.word.Word; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalSub.STLSub; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; +import java.util.List; + import static org.junit.jupiter.api.Assertions.assertEquals; class STLSubTest { - private IOSignal signal; + private IOSignal> signal; @BeforeEach void setUp() { @@ -24,7 +30,7 @@ void applyShortEventual() { @Test void applyShortGlobal() { - STLCost fml = new STLSub(new STLGlobal(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 10.0)), 1, 3); + STLCost fml = new STLSub(new STLGlobally(new STLOutputAtomic(0, STLOutputAtomic.Operation.gt, 10.0)), 1, 3); double expect = Double.POSITIVE_INFINITY; double actual = fml.apply(signal); assertEquals(expect, actual); diff --git a/core/src/test/java/net/maswag/STLUntilTest.java b/core/src/test/java/net/maswag/STLUntilTest.java index dde23d6c..185cae8a 100644 --- a/core/src/test/java/net/maswag/STLUntilTest.java +++ b/core/src/test/java/net/maswag/STLUntilTest.java @@ -1,6 +1,9 @@ package net.maswag; import net.automatalib.word.WordBuilder; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalUntil.STLUntil; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; diff --git a/core/src/test/java/net/maswag/SignalMapperTest.java b/core/src/test/java/net/maswag/SignalMapperTest.java index fc4578d1..b0d124d8 100644 --- a/core/src/test/java/net/maswag/SignalMapperTest.java +++ b/core/src/test/java/net/maswag/SignalMapperTest.java @@ -21,7 +21,7 @@ class SignalMapperTest { @BeforeEach void setUp() { - Function diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); + Function>, Double> diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); sigMap = new SignalMapper(Collections.singletonList(diff)); concreteSignal = new ArrayList<>(); concreteSignal.add(2.0); @@ -31,10 +31,10 @@ void setUp() { @Test void apply() { - assertEquals(6.2, sigMap.apply(0, new IOSignalPiece(Collections.emptyList(), concreteSignal))); + assertEquals(6.2, sigMap.apply(0, new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); // sigMap should be applied to an index smaller than the size of the SigMap. Otherwise, it throws IndexOutOfBoundsException. assertThrows(IndexOutOfBoundsException.class, () -> sigMap.apply(2, - new IOSignalPiece(Collections.emptyList(), concreteSignal))); + new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); } @Test @@ -47,14 +47,14 @@ void parse() throws IOException { sigMap = SignalMapper.parse(sigMapName); assertEquals(4, sigMap.size()); assertEquals(2.0 + 0.4, sigMap.apply(0, - new IOSignalPiece(Collections.emptyList(), concreteSignal))); + new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); assertEquals(-4.2 - 0.4 * 2.0, sigMap.apply(1, - new IOSignalPiece(Collections.emptyList(), concreteSignal))); + new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); assertEquals(0.5 + 2.0, sigMap.apply(2, - new IOSignalPiece(Collections.singletonList(0.5), concreteSignal))); + new IOSignalPiece<>(Collections.singletonList(0.5), concreteSignal))); assertEquals(abs(2.0 - 4.2), sigMap.apply(3, - new IOSignalPiece(Collections.emptyList(), concreteSignal))); + new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); assertThrows(IndexOutOfBoundsException.class, () -> sigMap.apply(4, - new IOSignalPiece(Collections.emptyList(), concreteSignal))); + new IOSignalPiece<>(Collections.emptyList(), concreteSignal))); } } \ No newline at end of file diff --git a/core/src/test/java/net/maswag/StaticSTLListTest.java b/core/src/test/java/net/maswag/StaticSTLListTest.java index 20ba6ac9..f369385e 100644 --- a/core/src/test/java/net/maswag/StaticSTLListTest.java +++ b/core/src/test/java/net/maswag/StaticSTLListTest.java @@ -10,9 +10,10 @@ import static org.hamcrest.MatcherAssert.assertThat; import static org.hamcrest.Matchers.containsInAnyOrder; import static org.junit.jupiter.api.Assertions.*; +import net.maswag.TemporalLogic.STLCost; class StaticSTLListTest { - private AdaptiveSTLUpdater properties; + private AdaptiveSTLUpdater> properties; @Nested class AutoTransTest { @@ -59,7 +60,7 @@ void setUp() { stlList = stlStringList.stream().map(stlString -> factory.parse(stlString, inputMapper, outputMapper, largest)).collect(Collectors.toList()); expectedStlStringList = stlList.stream().map(Object::toString).collect(Collectors.toList()); - properties = new StaticSTLList(stlList); + properties = new StaticSTLList<>(stlList); } @Test diff --git a/matlab/src/main/java/net/maswag/FalCAuN.java b/matlab/src/main/java/net/maswag/FalCAuN.java index 8121fb02..74628553 100644 --- a/matlab/src/main/java/net/maswag/FalCAuN.java +++ b/matlab/src/main/java/net/maswag/FalCAuN.java @@ -8,7 +8,16 @@ import net.automatalib.word.Word; import org.apache.commons.cli.MissingOptionException; import org.slf4j.LoggerFactory; - +import net.maswag.TemporalAnd.STLAnd; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalRelease.STLRelease; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalUntil.STLUntil; import java.io.FileOutputStream; import java.io.FileWriter; import java.nio.file.FileSystems; @@ -17,6 +26,7 @@ import java.util.stream.Collectors; import static net.maswag.ArgParser.EquivType.*; +import net.maswag.TemporalLogic.STLCost; /** *

FalCAuN class.

@@ -245,7 +255,7 @@ public static void main(String[] args) throws Exception { } } - private static void printResult(int i, List cexProperties, List cexConcreteInput, List> cexAbstractInput, List> cexOutput) { + private static >> void printResult(int i, List cexProperties, List cexConcreteInput, List> cexAbstractInput, List> cexOutput) { log.info("Property STL: {}", cexProperties.get(i).toString()); log.info("Property LTL: {}", cexProperties.get(i).toLTLString()); log.info("Concrete Input: {}", cexConcreteInput.get(i)); diff --git a/matlab/src/main/java/net/maswag/SimulinkRandomTester.java b/matlab/src/main/java/net/maswag/SimulinkRandomTester.java index 31c2e7d2..1b653254 100644 --- a/matlab/src/main/java/net/maswag/SimulinkRandomTester.java +++ b/matlab/src/main/java/net/maswag/SimulinkRandomTester.java @@ -5,6 +5,7 @@ import net.automatalib.alphabet.Alphabet; import net.automatalib.word.Word; import net.automatalib.word.WordBuilder; +import net.maswag.TemporalLogic.STLCost; import org.slf4j.LoggerFactory; import java.util.ArrayList; @@ -22,7 +23,7 @@ * @author Masaki Waga */ public class SimulinkRandomTester { - protected SUL, IOSignalPiece> simulink; + protected SUL, IOSignalPiece>> simulink; private final SimulinkSUL rawSimulink; private final Alphabet abstractInputAlphabet; private final NumericSULMapper mapper; @@ -103,7 +104,7 @@ public boolean run() { try { Word> concreteOutput = this.rawSimulink.execute(concreteInput); - IOSignal concreteSignal = new IOSignal(concreteInput, concreteOutput); + IOSignal> concreteSignal = new IOSignal<>(concreteInput, concreteOutput); LOGGER.debug("Abstract input: " + abstractInput); LOGGER.debug("Concrete output: " + concreteOutput); Iterator it = unfalsifiedIndex.iterator(); diff --git a/matlab/src/main/java/net/maswag/SimulinkSUL.java b/matlab/src/main/java/net/maswag/SimulinkSUL.java index 17a08a68..8d220000 100644 --- a/matlab/src/main/java/net/maswag/SimulinkSUL.java +++ b/matlab/src/main/java/net/maswag/SimulinkSUL.java @@ -18,7 +18,6 @@ import java.util.List; import java.util.Objects; import java.util.concurrent.ExecutionException; - /** * The System Under Learning implemented by a Simulink. We use the fixed step execution of Simulink to make sampling easier. */ @@ -106,7 +105,7 @@ public void post() { */ @Nullable @Override - public IOSignalPiece step(@Nullable List inputSignal) throws SULException { + public IOSignalPiece> step(@Nullable List inputSignal) throws SULException { assert (isInitial && endTime == 0) || (endTime > 0.0); if (inputSignal == null) { return null; @@ -158,7 +157,7 @@ public IOSignalPiece step(@Nullable List inputSignal) throws SULExceptio assert endTime > 0.0; LOGGER.trace("Output: " + result); - return new IOSignalPiece(inputSignal, result); + return new IOSignalPiece<>(inputSignal, result); } private void makeDataSet(StringBuilder builder) throws ExecutionException, InterruptedException { @@ -319,7 +318,7 @@ public Word> execute(Word> inputSignal) throws Interru */ @Nonnull @Override - public SUL, IOSignalPiece> fork() throws UnsupportedOperationException { + public SUL, IOSignalPiece>> fork() throws UnsupportedOperationException { throw new UnsupportedOperationException(); } diff --git a/matlab/src/test/java/net/maswag/AutotransExample.java b/matlab/src/test/java/net/maswag/AutotransExample.java index e13a4fc8..2a5c199b 100644 --- a/matlab/src/test/java/net/maswag/AutotransExample.java +++ b/matlab/src/test/java/net/maswag/AutotransExample.java @@ -1,10 +1,10 @@ package net.maswag; +import lombok.Getter; import org.apache.commons.collections4.CollectionUtils; import java.util.*; import java.util.function.Function; - /** * Example of the Automatic transmission model in HAF14 *

@@ -12,21 +12,28 @@ */ public class AutotransExample { private final String PWD = System.getenv("PWD"); + @Getter private final String initScript = "cd " + PWD + "/src/test/resources/MATLAB; initAT;"; + @Getter private final List paramNames = Arrays.asList("throttle", "brake"); private final int velocityIndex = 0; private final int rotationIndex = 1; private final int gearIndex = 2; - private List> abstractOutputs = new ArrayList<>(); - private List> concreteOutputs = new ArrayList<>(); + private final List> abstractOutputs = new ArrayList<>(); + private final List> concreteOutputs = new ArrayList<>(); private double signalStep; + @Getter private List> inputMapper; private List> outputMapper; + @Getter private List largest; private NumericSULVerifier verifier; - private AdaptiveSTLUpdater properties; + @Getter + private AdaptiveSTLUpdater> properties; + @Getter private NumericSULMapper mapper; - private List> sigMap = new ArrayList<>(); + @Getter + private List>, Double>> sigMap = new ArrayList<>(); AutotransExample(double signalStep) { this.signalStep = signalStep; @@ -101,10 +108,6 @@ private void setOutputMaps() { } } - public List> getInputMapper() { - return inputMapper; - } - void setInputMapper(List> inputMapper) { this.inputMapper = inputMapper; mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SignalMapper(sigMap)); @@ -120,24 +123,12 @@ void setOutputMapper(List> outputMapper) { setOutputMaps(); } - public List getLargest() { - return largest; - } - void setLargest(List largest) { this.largest = largest; mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SignalMapper(sigMap)); setOutputMaps(); } - public String getInitScript() { - return initScript; - } - - public List getParamNames() { - return paramNames; - } - public Double getSignalStep() { return signalStep; } @@ -146,23 +137,11 @@ NumericSULVerifier getVerifier() { return verifier; } - public AdaptiveSTLUpdater getProperties() { - return properties; - } - - void setProperties(AdaptiveSTLUpdater properties) { + void setProperties(AdaptiveSTLUpdater> properties) { this.properties = properties; } - public NumericSULMapper getMapper() { - return mapper; - } - - public List> getSigMap() { - return sigMap; - } - - public void setSigMap(List> sigMap) { + public void setSigMap(List>, Double>> sigMap) { this.sigMap = sigMap; mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SignalMapper(this.sigMap)); } diff --git a/matlab/src/test/java/net/maswag/NumericMembershipOracleTest.java b/matlab/src/test/java/net/maswag/NumericMembershipOracleTest.java index 3ebe2af0..37e44163 100644 --- a/matlab/src/test/java/net/maswag/NumericMembershipOracleTest.java +++ b/matlab/src/test/java/net/maswag/NumericMembershipOracleTest.java @@ -1,8 +1,8 @@ package net.maswag; import com.mathworks.engine.EngineException; -import de.learnlib.oracle.MembershipOracle; import de.learnlib.mapper.MappedSUL; +import de.learnlib.oracle.MembershipOracle; import de.learnlib.oracle.membership.SULOracle; import net.automatalib.alphabet.Alphabet; import net.automatalib.word.Word; @@ -27,9 +27,9 @@ class NumericMembershipOracleTest { private final Double signalStep = 10.0; private List properties; private NumericSULMapper mapper; - private List> sigMap = new ArrayList<>(); + private List>, Double>> sigMap = new ArrayList<>(); private SimulinkSUL simulink; - private MappedSUL, IOSignalPiece> mappedSimulink; + private MappedSUL, IOSignalPiece>> mappedSimulink; private MembershipOracle.MealyMembershipOracle sulOracle, directOracle; private Alphabet abstractInputAlphabet; private Alphabet> concreteInputAlphabet; diff --git a/matlab/src/test/java/net/maswag/SimulinkSULMapperTest.java b/matlab/src/test/java/net/maswag/SimulinkSULMapperTest.java index 691ad7a5..4756e3cd 100644 --- a/matlab/src/test/java/net/maswag/SimulinkSULMapperTest.java +++ b/matlab/src/test/java/net/maswag/SimulinkSULMapperTest.java @@ -8,7 +8,6 @@ import java.util.function.Function; import static org.junit.jupiter.api.Assertions.assertEquals; - class NumericSULMapperTest { private List> inputMapper; @@ -65,7 +64,7 @@ void mapOutput() { expected.put(new ArrayList<>(Arrays.asList(113.0, 200.0)), "00n"); for (Map.Entry, String> test : expected.entrySet()) { - String result = mapper.mapOutput(new IOSignalPiece(Collections.emptyList(), test.getKey())); + String result = mapper.mapOutput(new IOSignalPiece<>(Collections.emptyList(), test.getKey())); assertEquals(test.getValue(), result); } } @@ -86,8 +85,8 @@ void setUp() { mapper2.put('c', 100.0); inputMapper = new ArrayList<>(Arrays.asList(mapper1, mapper2)); } - Function diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); - List> sigMap = new ArrayList<>(Collections.singletonList(diff)); + Function>, Double> diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1); + List>, Double>> sigMap = new ArrayList<>(Collections.singletonList(diff)); List> outputMapper; List largest; { diff --git a/matlab/src/test/java/net/maswag/SimulinkSULTest.java b/matlab/src/test/java/net/maswag/SimulinkSULTest.java index 36161d9a..29d737eb 100644 --- a/matlab/src/test/java/net/maswag/SimulinkSULTest.java +++ b/matlab/src/test/java/net/maswag/SimulinkSULTest.java @@ -59,14 +59,14 @@ void post() { void step() { sul.pre(); List input = Arrays.asList(80.0, 900.0); - IOSignalPiece firstPair = sul.step(input); + IOSignalPiece> firstPair = sul.step(input); assert firstPair != null; List firstOutput = firstPair.getOutputSignal(); assertNotNull(firstOutput); assertEquals(expectedOutputSize, firstOutput.size()); input = Arrays.asList(85.0, 920.0); - IOSignalPiece secondPair = sul.step(input); + IOSignalPiece> secondPair = sul.step(input); assert secondPair != null; List secondOutput = secondPair.getOutputSignal(); assertNotNull(secondOutput); @@ -116,14 +116,14 @@ void post() { void step() { sul.pre(); List input = Arrays.asList(80.0, 0.0); - IOSignalPiece firstPair = sul.step(input); + IOSignalPiece> firstPair = sul.step(input); assert firstPair != null; List firstOutput = firstPair.getOutputSignal(); assertNotNull(firstOutput); assertEquals(expectedOutputSize, firstOutput.size()); input = Arrays.asList(0.0, 200.0); - IOSignalPiece secondPair = sul.step(input); + IOSignalPiece> secondPair = sul.step(input); assert secondPair != null; List secondOutput = secondPair.getOutputSignal(); assertNotNull(secondOutput); @@ -204,14 +204,14 @@ void post() { void step() { sul.pre(); List input = Arrays.asList(80.0, 0.0); - IOSignalPiece firstPair = sul.step(input); + IOSignalPiece> firstPair = sul.step(input); assert firstPair != null; List firstOutput = firstPair.getOutputSignal(); assertNotNull(firstOutput); assertEquals(expectedOutputSize, firstOutput.size()); input = Arrays.asList(0.0, 200.0); - IOSignalPiece secondPair = sul.step(input); + IOSignalPiece> secondPair = sul.step(input); assert secondPair != null; List secondOutput = secondPair.getOutputSignal(); assertNotNull(secondOutput); diff --git a/matlab/src/test/java/net/maswag/SimulinkSULVerifierTest.java b/matlab/src/test/java/net/maswag/SimulinkSULVerifierTest.java index c008cf07..5cc2cf04 100644 --- a/matlab/src/test/java/net/maswag/SimulinkSULVerifierTest.java +++ b/matlab/src/test/java/net/maswag/SimulinkSULVerifierTest.java @@ -11,7 +11,16 @@ import static org.hamcrest.Matchers.containsInAnyOrder; import static org.hamcrest.Matchers.greaterThan; import static org.junit.jupiter.api.Assertions.*; - +import net.maswag.TemporalAnd.STLAnd; +import net.maswag.TemporalEventually.STLEventually; +import net.maswag.TemporalGlobally.STLGlobally; +import net.maswag.TemporalImply.STLImply; +import net.maswag.TemporalLogic.STLCost; +import net.maswag.TemporalNext.STLNext; +import net.maswag.TemporalOr.STLOr; +import net.maswag.TemporalRelease.STLRelease; +import net.maswag.TemporalSub.STLSub; +import net.maswag.TemporalUntil.STLUntil; class SimulinkSULVerifierTest { private final String PWD = System.getenv("PWD"); private String initScript; @@ -23,10 +32,10 @@ class SimulinkSULVerifierTest { private final List paramNames = Arrays.asList("Pedal Angle", "Engine Speed"); private Double signalStep = 10.0; private SimulinkSULVerifier verifier; - private AdaptiveSTLUpdater properties; + private AdaptiveSTLUpdater> properties; private NumericSULMapper mapper; - private final List> sigMap = Collections.emptyList(); - private final AdaptiveSTLUpdater propertyZHA19_AFC1 = new StopDisprovedEQOracle.StaticLTLList(Collections.singletonList("X [] (output == \"a00l\" || output == \"a01l\" || output == \"a01h\" || output == \"b00l\" || output == \"b01l\" || output == \"b01h\" || output == \"b00l\" || output == \"b01l\" || output == \"b01h\"|| output == \"c00l\" || output == \"c01l\" || output == \"c01h\")")); + private final List>, Double>> sigMap = Collections.emptyList(); + private final AdaptiveSTLUpdater> propertyZHA19_AFC1 = new StopDisprovedEQOracle.StaticLTLList<>(Collections.singletonList("X [] (output == \"a00l\" || output == \"a01l\" || output == \"a01h\" || output == \"b00l\" || output == \"b01l\" || output == \"b01h\" || output == \"b00l\" || output == \"b01l\" || output == \"b01h\"|| output == \"c00l\" || output == \"c01l\" || output == \"c01h\")")); STLFactory factory = new STLFactory(); @BeforeEach @@ -59,7 +68,7 @@ void setUp() { } mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SignalMapper(sigMap)); // [] (velocity < 10) - properties = new StaticSTLList(Collections.singletonList( + properties = new StaticSTLList<>(Collections.singletonList( factory.parse("[] (signal(0) < 10.0)", inputMapper, outputMapper, largest))); try { @@ -122,9 +131,9 @@ void runZHA19_AFC1() { engineSpeedMapper.put('k', 1100.0); inputMapper = new ArrayList<>(Arrays.asList(pedalAngleMapper, engineSpeedMapper)); } - Function mu = a -> abs(a.getOutputSignal().get(0) - + Function>, Double> mu = a -> abs(a.getOutputSignal().get(0) - a.getOutputSignal().get(1)) / a.getOutputSignal().get(1); - List> sigMap = new ArrayList<>(Collections.singletonList(mu)); + List>, Double>> sigMap = new ArrayList<>(Collections.singletonList(mu)); { Map afMapper = new HashMap<>(); afMapper.put('a', 10.0); @@ -206,9 +215,9 @@ void runHAF14_AT4() { engineSpeedMapper.put('k', 1100.0); inputMapper = new ArrayList<>(Arrays.asList(pedalAngleMapper, engineSpeedMapper)); } - Function mu = + Function>, Double> mu = a -> abs(a.getOutputSignal().get(0) - a.getOutputSignal().get(1)) / a.getOutputSignal().get(1); - List> sigMap = new ArrayList<>(Collections.singletonList(mu)); + List>, Double>> sigMap = new ArrayList<>(Collections.singletonList(mu)); { Map afMapper = new HashMap<>(); afMapper.put('a', 10.0); @@ -253,7 +262,7 @@ void runHAF14_AT4() { @Test void getCexProperty() { assertFalse(verifier.run()); - List expected = properties.getSTLProperties(); + List>> expected = properties.getSTLProperties(); assertEquals(expected, verifier.getCexProperty()); } @@ -306,7 +315,7 @@ void setTimeout() throws Exception { // generate properties String stlString = "alw_[0, 3] (signal(1) < 4750)"; STLCost stl = factory.parse(stlString, inputMapper, outputMapper, largest); - properties = new StaticSTLList(Collections.singletonList(stl)); + properties = new StaticSTLList<>(Collections.singletonList(stl)); // define the verifier verifier = new SimulinkSULVerifier(initScript, paramNames, signalStep, 0.0025, properties, mapper); // set timeout @@ -334,13 +343,13 @@ void setUp() { @Test void runStatic() { // generate properties - properties = new StaticSTLList(Collections.singletonList(stl)); + properties = new StaticSTLList<>(Collections.singletonList(stl)); } @Test void runAdaptive() { // generate properties - properties = new AdaptiveSTLList(Collections.singletonList(stl)); + properties = new AdaptiveSTLList<>(Collections.singletonList(stl)); } @AfterEach @@ -372,14 +381,14 @@ void setUp() { @Test void runStatic() throws Exception { // generate properties - properties = new StaticSTLList(stlList); + properties = new StaticSTLList<>(stlList); verify(); } @Test void runAdaptive() throws Exception { // generate properties - properties = new AdaptiveSTLList(stlList); + properties = new AdaptiveSTLList<>(stlList); verify(); }