minor tweaks

falstar/src/falstar/falsification/Validation.scala

@@ -17,6 +17,8 @@ object Validation {
     if(ok) "yes" else "no"
   }
 
+  val isTrue = Set("1", "true", "yes")
+
   def apply(table: Table, parser: Parser): Seq[Row] = {
     for(row <- table.rows) yield {
       val res = apply(row, parser)
@@ -37,7 +39,6 @@ object Validation {
     val falstar.parser.Node(node) = falstar.parser.read(property)
     state.system = sys // such that ports and stuff work
     val phi = parser.formula(node)
-    val T = phi.T
 
     val res = mutable.Buffer[(String, Any)]()
 
@@ -47,7 +48,12 @@ object Validation {
 
     if(data contains "input") {
         val ps = Vector.parse(data.getOrElse("parameters", "[]"))
-        val us = Signal.parse(data("input"))
+
+        val us = if(data contains "times") {
+          Signal.parse(data("times"), data("input"))
+        } else {
+          Signal.parse(data("input"))
+        }
         // res += "input" -> input
 
         val pr = cfg.pn(sys.params)
@@ -56,12 +62,18 @@ object Validation {
         val ur = cfg.in(sys.inputs)
         res += "inputs valid" -> check(us forall { case (t, x) => ur contains x })
 
+        val T = if(data contains "time horizon") {
+            data("time horizon").toDouble
+        } else {
+            phi.T
+        }
+
         val tr = sys.sim(ps, us, T)
         val rs = Robustness(phi, tr.us, tr.ys)
 
         if(data contains "falsified") {
             val expected = data("falsified")
-            res += "falsified correct" -> check(expected == check(rs.score < 0))
+            res += "falsified correct" -> check(isTrue(expected) == (rs.score < 0))
         }
 
         if(data contains "robustness") {

falstar/src/falstar/hybrid/Signal.scala

@@ -6,24 +6,28 @@ import falstar.linear.Vector
 
 object Signal {
   def parse(str: String): Signal = {
-    assert(str startsWith "[")
-    assert(str endsWith "]")
-    val inner = str.substring(1, str.length - 1)
-
-    if(inner.isEmpty) {
-      Signal.empty
-    } else {
-      val points = inner.split(";")
-
-      for(point <- points) yield {
-        val x = point.trim.split("\\s+")
-        val t = x(0).toDouble
-        val y = Vector(x.length - 1, i => x(i + 1).toDouble)
-        (t, y)
-      }
+    for(x <- falstar.util.splitMatlab2(str)) yield {
+      val t = x(0).toDouble
+      val y = Vector(x.length - 1, i => x(i + 1).toDouble)
+      (t, y)
+    }
+  }
+
+  def parse(times: String, points: String): Signal = {
+    val ts = falstar.util.splitMatlab1(times)
+    val xs = falstar.util.splitMatlab2(points)
+    assert(ts.length == xs.length)
+    for((t,x) <- (ts zip xs)) yield {
+      val y = Vector(x.length, i => x(i).toDouble)
+      (t.toDouble, y)
     }
   }
 
+  def zip(ts: Vector, xs: Seq[Vector]): Signal = {
+    assert(ts.length == xs.length)
+    ts.data zip xs
+  }
+
   def length(t0: Time, dt: Duration, T: Time): Int = {
     Math.ceil((T - t0) / dt).toInt
   }

falstar/src/falstar/linear/Vector.scala

@@ -132,15 +132,8 @@ object Vector {
   }
 
   def parse(str: String): Vector = {
-    assert(str startsWith "[")
-    assert(str endsWith "]")
-    val inner = str.substring(1, str.length - 1).trim
-    if(inner.isEmpty) {
-      empty
-    } else {
-      val data = inner.trim.split("\\s+")
-      Vector(data.length, i => data(i).toDouble)
-    }
+    val data = falstar.util.splitMatlab1(str)
+    Vector(data.length, i => data(i).toDouble)
   }
 
   def apply(length: Int, init: (Int) => Double): Vector = {

falstar/src/falstar/util/package.scala

@@ -12,6 +12,35 @@ package object util {
     df.format(new Date());
   }
 
+  def splitMatlab1(str: String): Array[String] = {
+    assert(str startsWith "[")
+    assert(str endsWith "]")
+    val inner = str.substring(1, str.length - 1).trim
+    if(inner.isEmpty) {
+      Array()
+    } else {
+      inner.split("\\s+")
+    }
+  }
+
+  def splitMatlab2(str: String): Array[Array[String]] = {
+    assert(str startsWith "[")
+    assert(str endsWith "]")
+    val inner = str.substring(1, str.length - 1).trim
+    if(inner.isEmpty) {
+      Array()
+    } else {
+      val parts = inner.split(";")
+      for(part <- parts) yield {
+        val part_ = part.trim
+        if(part_.isEmpty)
+          Array[String]()
+        else
+          part_.split("\\s+")
+      }
+    }
+  }
+
   def time[A](m: String, f: => A) = {
     val start = java.lang.System.currentTimeMillis()
     val r = f