Commit bed7ccbd authored by Christian Müller's avatar Christian Müller

add ts output

parent ca549501
......@@ -7,7 +7,7 @@ import java.io.PrintWriter
import de.tum.niwo.toz3.Z3BSFO
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.graphs.WFGraphEncoding
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.invariants.{InvProperties, InvariantChecker}
object Utils extends LazyLogging {
......@@ -98,7 +98,11 @@ object Utils extends LazyLogging {
val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
Utils.write(name, s"${filenames}_workflow.dot", elabdot)
val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
val tsgraph = TSGraphEncoding.toGraph(invspec.ts)
val elabtsdot = TSGraphEncoding.toDot(tsgraph)(Map(), Set())
Utils.write(name, s"${filenames}_ts.dot", elabtsdot)
infer(name, desc, invspec, properties)
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment