This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

NaiveCoupledSimCheck.scala 957 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
package de.bbisping.coupledsim.checkers

import de.bbisping.coupledsim.util.Relation
import de.bbisping.coupledsim.ts.WeakTransitionSystem

/** checks, whether a relation is a coupled simulation w.r.t some transition system and throws counter examples.*/
class NaiveCoupledSimCheck[S, A, L] (
    ts: WeakTransitionSystem[S, A, L],
    rel: Relation[S]) {
  
  def check() = {
    (checkSimulation() map ((_, "violates simulation"))) ++
      (checkCoupling() map ((_, "violates coupling")))
  }
  
  def checkSimulation() = {
    rel.tupleSet filterNot {
      case (p, q) =>
        ts.post(p) forall {
          case (a, p1s) =>
            p1s forall { p1 =>
              ts.weakPost(q, a) exists {
                q1 => rel(p1, q1)
              }
            }
        }
    }
  }
  
  def checkCoupling() = {
    rel.tupleSet filterNot {
      case (p, q) =>
        ts.silentReachable(q) exists { q1 =>
          rel(q1, p)
        }
    }
  }
  
}