Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

added license and support for UNTIL operator to verification extension

  • Loading branch information...
commit 6865e49f745edabbf9a5ad8293161de6bdf81ea8 1 parent 852c42f
@papousek papousek authored
View
4 ...ava/org/sybila/parasim/computation/verification/stl/cpu/AbstractUnaryTemporalMonitor.java
@@ -36,15 +36,11 @@
*/
public abstract class AbstractUnaryTemporalMonitor extends AbstractMonitor {
- private final Monitor subMonitor;
- private final FormulaInterval interval;
private final List<Robustness> robustnesses;
public AbstractUnaryTemporalMonitor(Monitor subMonitor, FormulaInterval interval) {
Validate.notNull(interval);
Validate.notNull(subMonitor);
- this.subMonitor = subMonitor;
- this.interval = interval;
this.robustnesses = precomputeRobustness(subMonitor, interval);
}
View
3  .../src/main/java/org/sybila/parasim/computation/verification/stl/cpu/STLMonitorFactory.java
@@ -26,6 +26,7 @@
import org.sybila.parasim.model.verification.stl.FutureFormula;
import org.sybila.parasim.model.verification.stl.GloballyFormula;
import org.sybila.parasim.model.verification.stl.Predicate;
+import org.sybila.parasim.model.verification.stl.UntilFormula;
/**
* @author <a href="mailto:xpapous1@fi.muni.cz">Jan Papousek</a>
@@ -49,6 +50,8 @@ public Monitor createMonitor(Trajectory trajectory, Formula property) {
return new OrMonitor(createMonitor(trajectory, property.getSubformula(0)), createMonitor(trajectory, property.getSubformula(1)));
case PREDICATE:
return new PredicateMonitor(trajectory, (Predicate) property);
+ case UNTIL:
+ return new UntilMonitor(createMonitor(trajectory, property.getSubformula(0)), createMonitor(trajectory, property.getSubformula(1)), ((UntilFormula) property).getInterval());
default:
throw new UnsupportedOperationException("There is no available monitor for formula type [" + property.getType() + "].");
}
View
91 ...-impl/src/main/java/org/sybila/parasim/computation/verification/stl/cpu/UntilMonitor.java
@@ -0,0 +1,91 @@
+/**
+ * Copyright 2011 - 2012, Sybila, Systems Biology Laboratory and individual
+ * contributors by the @authors tag.
+ *
+ * This file is part of Parasim.
+ *
+ * Parasim is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+package org.sybila.parasim.computation.verification.stl.cpu;
+
+import java.util.ArrayList;
+import java.util.List;
+import org.sybila.parasim.computation.verification.cpu.AbstractMonitor;
+import org.sybila.parasim.computation.verification.cpu.Monitor;
+import org.sybila.parasim.model.verification.Robustness;
+import org.sybila.parasim.model.verification.SimpleRobustness;
+import org.sybila.parasim.model.verification.stl.FormulaInterval;
+
+/**
+ * @author <a href="mailto:xpapous1@fi.muni.cz">Jan Papousek</a>
+ */
+public class UntilMonitor extends AbstractMonitor {
+
+ private final List<Robustness> robustnesses;
+
+ public UntilMonitor(Monitor left, Monitor right, FormulaInterval interval) {
+ if (left == null) {
+ throw new IllegalArgumentException("The parameter [left] is null.");
+ }
+ if (right == null) {
+ throw new IllegalArgumentException("The parameter [right] is null.");
+ }
+ if (interval == null) {
+ throw new IllegalArgumentException("The parameter [interval] is null.");
+ }
+ robustnesses = precompute(left, right, interval);
+ }
+
+ public Robustness getRobustness(int index) {
+ return robustnesses.get(index);
+ }
+
+ public int size() {
+ return robustnesses.size();
+ }
+
+ private List<Robustness> precompute(Monitor left, Monitor right, FormulaInterval interval) {
+ int current = 0;
+ boolean finished = false;
+ List<Robustness> precomputed = new ArrayList<Robustness>();
+ int shortestSize = Math.min(left.size(), right.size());
+ while (current < shortestSize) {
+ int windowEnd = current;
+ float currentTime = left.getRobustness(windowEnd).getTime();
+ float windowEndLeft = left.getRobustness(windowEnd).getValue();
+ while (windowEnd < shortestSize - 1 && left.getRobustness(windowEnd).getTime() < currentTime + interval.getLowerBound()) {
+ windowEnd++;
+ windowEndLeft = Math.min(windowEndLeft, left.getRobustness(windowEnd).getValue());
+ }
+ if (left.getRobustness(windowEnd).getTime() < interval.getLowerBound()) {
+ break;
+ }
+ float windowEndRight = right.getRobustness(windowEnd).getValue();
+ float currentRobustness = Math.min(windowEndLeft, windowEndRight);
+ while(windowEnd < shortestSize - 1 && left.getRobustness(windowEnd + 1).getTime() <= currentTime + interval.getUpperBound()) {
+ windowEnd++;
+ windowEndLeft = Math.min(windowEndLeft, left.getRobustness(windowEnd).getValue());
+ windowEndRight = right.getRobustness(windowEnd).getValue();
+ currentRobustness = Math.max(currentRobustness, Math.min(windowEndLeft, windowEndRight));
+ }
+ if (left.getRobustness(windowEnd).getTime() < currentTime + interval.getUpperBound() && windowEnd == shortestSize - 1) {
+ break;
+ }
+ precomputed.add(new SimpleRobustness(currentRobustness, left.getRobustness(current).getTime()));
+ current++;
+ }
+ return precomputed;
+ }
+
+}
View
34 ...src/test/java/org/sybila/parasim/computation/verification/TestSTLFormulaVerification.java
@@ -1,5 +1,25 @@
+/**
+ * Copyright 2011 - 2012, Sybila, Systems Biology Laboratory and individual
+ * contributors by the @authors tag.
+ *
+ * This file is part of Parasim.
+ *
+ * Parasim is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
package org.sybila.parasim.computation.verification;
+import org.sybila.parasim.model.verification.stl.UntilFormula;
import org.sybila.parasim.model.verification.stl.OrFormula;
import java.util.ArrayList;
import java.util.HashMap;
@@ -91,6 +111,20 @@ public void testOr() {
assertEquals(verified.getRobustness(0).getValue(), -1f);
}
+ @Test
+ public void testUntil() {
+ Formula formula = new UntilFormula(
+ createPredicate(createMapping(), Type.GREATER, 9),
+ createPredicate(createMapping(), Type.LESSER, 15),
+ new TimeInterval(2, 4, IntervalBoundaryType.CLOSED)
+ );
+ STLVerifier verifier = getManager().resolve(STLVerifier.class, Default.class, getManager().getRootContext());
+ VerifiedDataBlock verified = verifier.verify(
+ new ArrayDataBlock<Trajectory>(new Trajectory[] { createTrajectory(10, 10, 16, 12, 15, 9) }),
+ formula);
+ assertEquals(verified.getRobustness(0).getValue(), 1f);
+ }
+
private Trajectory createTrajectory(float...oneDimensionPoints) {
List<Point> points = new ArrayList<Point>();
for (int i=0; i<oneDimensionPoints.length; i++) {
View
1  ...mpl/src/test/java/org/sybila/parasim/computation/verification/stl/cpu/TestNotMonitor.java
@@ -20,7 +20,6 @@
package org.sybila.parasim.computation.verification.stl.cpu;
import org.sybila.parasim.computation.verification.cpu.Monitor;
-import org.sybila.parasim.computation.verification.stl.cpu.NotMonitor;
import org.testng.annotations.Test;
import static org.testng.Assert.*;
View
45 ...l/src/test/java/org/sybila/parasim/computation/verification/stl/cpu/TestUntilMonitor.java
@@ -0,0 +1,45 @@
+/**
+ * Copyright 2011 - 2012, Sybila, Systems Biology Laboratory and individual
+ * contributors by the @authors tag.
+ *
+ * This file is part of Parasim.
+ *
+ * Parasim is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
+ */
+package org.sybila.parasim.computation.verification.stl.cpu;
+
+import org.sybila.parasim.computation.verification.cpu.Monitor;
+import org.sybila.parasim.model.verification.stl.IntervalBoundaryType;
+import org.sybila.parasim.model.verification.stl.TimeInterval;
+import org.testng.annotations.Test;
+import static org.testng.Assert.*;
+
+/**
+ * @author <a href="mailto:xpapous1@fi.muni.cz">Jan Papousek</a>
+ */
+public class TestUntilMonitor extends AbstractMonitorTest {
+
+ @Test
+ public void testUntilMonitor() {
+ Monitor left = createTestMonitor(1, 2, 3, 4, 3, 2, -10);
+ Monitor right = createTestMonitor(2, 1, -10, 3, 9, 0, 0);
+ Monitor until = new UntilMonitor(left, right, new TimeInterval(2, 4, IntervalBoundaryType.CLOSED));
+ Monitor expected = createTestMonitor(1, 2, 3);
+ assertEquals(until.size(), expected.size());
+ for (int i=0; i<expected.size(); i++) {
+ assertEquals(until.getRobustness(i).getValue(), expected.getRobustness(i).getValue(), "The robustness doesn't match in index <" + i + ">.");
+ }
+ }
+
+}
Please sign in to comment.
Something went wrong with that request. Please try again.