log validation some cool stetps

ERATOMMSD · May 11, 2021 · 9f5bdc3 · 9f5bdc3
1 parent 335221d
commit 9f5bdc3
Show file tree

Hide file tree

Showing 16 changed files with 437 additions and 290 deletions.
diff --git a/build.sc b/build.sc
@@ -0,0 +1,10 @@
+import mill._
+import mill.scalalib._
+
+object falstar extends ScalaModule {
+    def scalaVersion = "2.12.13"
+    def mainClass = Some("falstar.Main")
+
+    def ivyDeps = Agg(
+        ivy"org.apache.commons:commons-csv:1.8")
+}
diff --git a/falstar-config.sh b/falstar-config.sh
@@ -22,6 +22,8 @@ then
 # Bring $MATLABROOT into the environment
     source ~/.falstar/matlab
     echo "Matlab at: $MATLABROOT"
+    export LD_LIBRARY_PATH="$MATLABROOT/bin/glnxa64:$MATLABROOT/sys/os/glnxa64"
+    MATLABJARS="$MATLABROOT/java/jar/mvm.jar:$MATLABROOT/java/jar/javaenginecore.jar:$MATLABROOT/java/jar/matlab.jar:$MATLABROOT/java/jar/engine.jar:$MATLABROOT/java/jar/util.jar:$MATLABROOT/java/jar/capabilities.jar"
 else
     echo "Could not determine Matlab installation."
 fi

diff --git a/falstar-scala.sh b/falstar-scala.sh
@@ -1,10 +1,5 @@
 #!/bin/sh
 
 HERE=`dirname "$0"`
-
-source ~/.falstar/matlab
-export LD_LIBRARY_PATH="$MATLABROOT/bin/glnxa64:$MATLABROOT/sys/os/glnxa64"
-
-CP="$MATLABROOT/java/jar/mvm.jar:$MATLABROOT/java/jar/javaenginecore.jar:$MATLABROOT/java/jar/matlab.jar:$MATLABROOT/java/jar/engine.jar:$MATLABROOT/java/jar/util.jar:$MATLABROOT/java/jar/capabilities.jar"
-
-./scala-2.12.13/bin/scala -cp "$CP:$HERE/falstar.jar" $@
+source $HERE/falstar-config.sh
+scala -cp "$MATLABJARS:$HERE/falstar.jar" $@
diff --git a/falstar-session.sh b/falstar-session.sh
@@ -1,10 +1,5 @@
 #!/bin/sh
 
 HERE=`dirname "$0"`
-
-source ~/.falstar/matlab
-export LD_LIBRARY_PATH="$MATLABROOT/bin/glnxa64:$MATLABROOT/sys/os/glnxa64"
-
-CP="$MATLABROOT/java/jar/mvm.jar:$MATLABROOT/java/jar/javaenginecore.jar:$MATLABROOT/java/jar/matlab.jar:$MATLABROOT/java/jar/engine.jar:$MATLABROOT/java/jar/util.jar:$MATLABROOT/java/jar/capabilities.jar"
-
-./scala-2.12.13/bin/scala -cp "$CP:$HERE/falstar.jar" falstar.util.Matlab $@
+source $HERE/falstar-config.sh
+java -cp "$MATLABJARS:$HERE/falstar.jar" falstar.util.Matlab $@
diff --git a/falstar.sh b/falstar.sh
@@ -1,11 +1,5 @@
 #!/bin/sh
 
 HERE=`dirname "$0"`
-
 source $HERE/falstar-config.sh
-
-export LD_LIBRARY_PATH="$MATLABROOT/bin/glnxa64:$MATLABROOT/sys/os/glnxa64"
-
-CP="$MATLABROOT/java/jar/mvm.jar:$MATLABROOT/java/jar/javaenginecore.jar:$MATLABROOT/java/jar/matlab.jar:$MATLABROOT/java/jar/engine.jar:$MATLABROOT/java/jar/util.jar:$MATLABROOT/java/jar/capabilities.jar"
-
-java -cp "$CP:$HERE/falstar.jar" falstar.Main $@
+java -cp "$MATLABJARS:$HERE/falstar.jar" falstar.Main $@
diff --git a/falstar/src/falstar/Main.scala b/falstar/src/falstar/Main.scala
@@ -15,12 +15,14 @@ import falstar.parser.Flush
 import falstar.parser.Quit
 import falstar.parser.Robustness
 import falstar.parser.Simulate
+import falstar.parser.Validate
 import falstar.parser.parse
 import falstar.util.Probability
 import falstar.util.Row
 import falstar.util.Scope
 import falstar.util.Matlab
 import falstar.util.Table
+import falstar.falsification.Validation
 
 object Main {
   object quit extends Breaks
@@ -31,6 +33,7 @@ object Main {
     var graphics = false
     var dummy = false
     var append = true
+    var args: List[String] = Nil
   }
 
   val results = mutable.Map[String, mutable.Buffer[Row]]()
@@ -66,6 +69,16 @@ object Main {
         val scope = new Scope(title, sys, best)
       }
 
+    case Validate(log, report, parser) =>
+      val table = Table.read(log.get)
+      val rows = Validation.apply(table, parser)
+
+      for (name <- report) {
+        if (!(results contains name))
+          results(name) = mutable.Buffer()
+        results(name) ++= rows
+      }
+
     case Simulate(sys, phi, ps, us, t) =>
       val tr = sys.sim(ps, us, t)
       val rs = mtl.Robustness(phi, tr.us, tr.ys)
@@ -110,7 +123,6 @@ object Main {
     }
   }
 
-  @tailrec
   def setup(args: List[String]): List[String] = args match {
     case "-a" :: rest =>
       options.ask = true
@@ -125,8 +137,13 @@ object Main {
     case "-d" :: rest =>
       options.dummy = true
       setup(rest)
-    case _ =>
-      args
+    case "--" :: rest =>
+      options.args = rest
+      Nil
+    case Nil =>
+      Nil
+    case file :: rest =>
+      file :: setup(rest)
   }
 
   def safe(f: => Any) = {
@@ -161,36 +178,14 @@ object Main {
 
   def main(args: Array[String]) {
     if (args.isEmpty) {
-      println("usage: falstar [-agv] [+] file_1 ... file_n")
-      println("  -a    ask for additional input files:")
-      println("          enter one filename per line followed by a blank line")
-      println("          a blank line acknowledges, EOF (CTRL+d) aborts")
-      println("  -d    dummy run, parse and validate configuration only")
-      println("  -g    show a graphical diagram for each trial")
-      println("  -v    be verbose")
-      println("   +    no header in csv for next file (data should match previous header)")
+      println("usage: falstar [-dv] file_1 ... file_n")
+      println("  -d    parse configuration only")
+      println("  -v    be more verbose")
     }
 
-    val rest = setup(args.toList)
-
-    var files = Buffer[String]()
-    files ++= rest
-
-    quit.breakable {
-      while (options.ask) {
-        val line = StdIn.readLine
-
-        if (line == null)
-          quit.break
-        else if (line.isEmpty)
-          options.ask = false
-        else
-          files += line
-      }
-
-      runall(files)
-      writeall(results)
-    }
+    val files = setup(args.toList)
+    runall(files)
+    writeall(results)
 
     println("bye")
 

diff --git a/falstar/src/falstar/falsification/Falsification.scala b/falstar/src/falstar/falsification/Falsification.scala
@@ -19,15 +19,17 @@ trait Falsification {
       case Some(seed) => Probability.seed = seed
     }
 
-    val time = now()
+    val start = now()
 
     val data = (1 to n) map {
       i =>
         println("trial " + i + "/" + n)
-        val (res, stat, row) = apply(sys, cfg, phi)
+        val (res, stat, row) = apply(sys, cfg, phi, notes)
         ((res, stat), row)
     }
 
+    val end = now()
+
     val (all, rows) = data.unzip
 
     val (best, _) = all.minBy(_._1.score)
@@ -44,7 +46,8 @@ trait Falsification {
 
     val what = Seq(
       "model" -> sys.name, "formula" -> phi,
-      "start date" -> time
+      "start date" -> start,
+      "end date" -> end
     )
 
     val how = Seq(
@@ -61,7 +64,7 @@ trait Falsification {
     (best, good map (_._1.tr.us), rows, Row(what ++ notes ++ how ++ params ++ aggregate))
   }
 
-  def apply(sys: System, cfg: Config, phi: Formula): (Result, Statistics, Row) = {
+  def apply(sys: System, cfg: Config, phi: Formula, notes: Seq[(String, Any)]): (Result, Statistics, Row) = {
     val seed = Probability.seed
 
     println("property " + phi)
@@ -72,7 +75,10 @@ trait Falsification {
       println("  " + name + ": " + value)
     }
 
+    val start = now()
     val (res, stats) = search(sys, cfg, phi)
+    val end = now()
+
     println()
 
     println("inputs")
@@ -101,14 +107,23 @@ trait Falsification {
     println("  peak memory " + falstar.util.peakMemBytes / 1000 + " kb")
     println()
 
+    val what = Seq(
+      "model" -> sys.name, "formula" -> phi,
+      "start date" -> start,
+      "end date" -> end
+    )
+
+    val how = Seq(
+       "algorithm" -> this.identification,
+    )
+
     val data = Seq(
-      "model" -> sys.name, "property" -> phi, "algorithm" -> this.identification,
       "seed" -> seed, "simulations" -> stats.simulations, "time" -> stats.time, "robustness" -> res.score,
       "falsified" -> { if (res.isFalsified) "yes" else "no" },
       "input" -> { if (!us.isEmpty) (us toMatlab T) else "[]" },
       "output" -> { if (!ys.isEmpty) (ys toMatlab T) else "[]" })
 
-    val row = Row(data ++ params)
+    val row = Row(what ++ notes ++ how ++ params ++ data)
 
     // expose another seed for the next trial
     // required for external algorithms (Breach, S-Taliro)

diff --git a/falstar/src/falstar/falsification/Validation.scala b/falstar/src/falstar/falsification/Validation.scala
@@ -0,0 +1,82 @@
+package falstar.falsification
+
+import scala.collection.mutable
+
+import falstar.util.Row
+import falstar.util.Table
+import falstar.hybrid.Config
+import falstar.mtl.Formula
+import falstar.mtl.Robustness
+import falstar.hybrid.System
+import falstar.parser.Parser
+import falstar.hybrid.Signal
+import falstar.linear.Vector
+
+object Validation {
+  def check(ok: Boolean) = {
+    if(ok) "yes" else "no"
+  }
+
+  def apply(table: Table, parser: Parser): Seq[Row] = {
+    for(row <- table.rows) yield {
+      val res = apply(row, parser)
+      print(".")
+      res
+    }
+  }
+
+  def apply(row: Row, parser: Parser): Row = {
+    val data = row.data.toMap.asInstanceOf[Map[String,String]]
+
+    val system = data("system")
+    val state = parser.state
+    val (sys, cfg) = state.systems(system)
+
+    val property = data("property")
+    // need to unpack one layer because it reads a sequence of nodes
+    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)]()
+
+    res += "system" -> system
+    res += "property" -> property
+    res += "formula" -> phi
+
+    if(data contains "input") {
+        val ps = Vector.parse(data.getOrElse("parameters", "[]"))
+        val us = Signal.parse(data("input"))
+        // res += "input" -> input
+
+        val pr = cfg.pn(sys.params)
+        res += "parameters valid" -> check(pr contains ps)
+
+        val ur = cfg.in(sys.inputs)
+        res += "inputs valid" -> check(us forall { case (t, x) => ur contains x })
+
+        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))
+        }
+
+        if(data contains "robustness") {
+            val expected = data("robustness").toDouble
+            val computed = rs.score
+            val error = Math.abs(expected - computed)
+            res += "robustness correct" -> check((expected < 0) == (computed < 0))
+            res += "robustness error" -> error
+        }
+
+        if(data contains "output") {
+          val ys = Signal.parse(data("output"))
+        }
+    }
+
+    Row(res)
+  }
+}
diff --git a/falstar/src/falstar/hybrid/Signal.scala b/falstar/src/falstar/hybrid/Signal.scala
@@ -5,6 +5,25 @@ import scala.collection.mutable.ArrayBuffer
 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)
+      }
+    }
+  }
+
   def length(t0: Time, dt: Duration, T: Time): Int = {
     Math.ceil((T - t0) / dt).toInt
   }
@@ -39,7 +58,7 @@ object Signal {
     val us = Seq.tabulate(controlpoints)(i => x)
     Signal(steps, i => (t0 + i * dt, us(i * controlpoints / steps)))
   }
-  
+
   implicit class SignalOps(xs: Signal) {
     def t0: Time = {
       if (xs.isEmpty) 0

diff --git a/falstar/src/falstar/linear/Vector.scala b/falstar/src/falstar/linear/Vector.scala
@@ -128,7 +128,19 @@ class Vector(val length: Int) extends Traversable[Double] {
 
 object Vector {
   val empty = {
-    Vector(0)
+    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)
+    }
   }
 
   def apply(length: Int, init: (Int) => Double): Vector = {