Commit 8542dd8d authored by Christian Müller's avatar Christian Müller

finite sorts

parent 37bd0626
...@@ -154,7 +154,7 @@ class Z3Test extends FlatSpec with LazyLogging { ...@@ -154,7 +154,7 @@ class Z3Test extends FlatSpec with LazyLogging {
logger.info(s"Using universe $universe") logger.info(s"Using universe $universe")
val quantfree = LTL.eliminateUniversals(res, agents) val quantfree = LTL.eliminateUniversals(res, agents)
// val ltlprop = LTL.eliminatePredicates(quantfree) val ltlprop = LTL.eliminatePredicates(quantfree)
val mapped = agents.groupBy(v => v.typ) val mapped = agents.groupBy(v => v.typ)
val ctx = new Context() val ctx = new Context()
......
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