TSInstantiator.scala 806 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
package de.tum.niwo.blocks

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.FOLTL.Var
import de.tum.niwo.foltl.FOTransformers

object InvSpecInstantiator extends LazyLogging {

  def instantiate(spec:InvariantSpec, universe:Map[String, List[Var]]) = {

    val newaxioms = FOTransformers.eliminateQuantifiers(spec.axioms, universe)
    val newinv = FOTransformers.eliminateQuantifiers(spec.inv, universe)

    val tsblocks = spec.ts.steps.map(_.mapStatements(
      stmt => stmt.update(guard = FOTransformers.eliminateQuantifiers(stmt.guard, universe))
    ))
    val newsig = spec.ts.sig.copy(constants = spec.ts.sig.constants ++ universe.values.flatten)
    val newts = spec.ts.copy(steps = tsblocks, sig = newsig)

    spec.copy(ts = newts, axioms = newaxioms, inv = newinv)
  }

}