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 📥

Commit 1d1dfef9 by benkeks

Merge branch 'master' into 'master'

TACAS 2019 Changes

See merge request !1
parents 80d4598e 2ef57139
......@@ -2,7 +2,7 @@ name := "CoupledSim"
version := "0.1.0"
scalaVersion := "2.11.12"
scalaVersion := "2.12.8"
val scalacOpts = Seq(
"-Xmax-classfile-name", "140",
......@@ -13,7 +13,7 @@ val scalacOpts = Seq(
)
lazy val web = (project in file("web")).settings(
scalaVersion := "2.11.12",
scalaVersion := "2.12.8",
scalaJSProjects := Seq(jsClient),
isDevMode in scalaJSPipeline := false,
pipelineStages in Assets := Seq(scalaJSPipeline),
......@@ -26,7 +26,7 @@ lazy val web = (project in file("web")).settings(
).enablePlugins(SbtWeb)
lazy val shared = (project in file("shared")).settings(
scalaVersion := "2.11.12",
scalaVersion := "2.12.8",
name := "shared",
scalacOptions ++= scalacOpts,
test in assembly := {},
......@@ -36,7 +36,7 @@ lazy val shared = (project in file("shared")).settings(
)
lazy val jsClient = (project in file("js-client")).settings(
scalaVersion := "2.11.12",
scalaVersion := "2.12.8",
name := "coupledsim-client",
parallelExecution in ThisBuild := false,
scalacOptions ++= scalacOpts,
......@@ -59,20 +59,20 @@ lazy val jsClient = (project in file("js-client")).settings(
"org.webjars" % "bootstrap" % "3.3.7" / "bootstrap.min.js"
),
unmanagedSourceDirectories in Compile +=
baseDirectory.value / ".." / "shared" / "src" / "main" / "scala-2.11"
baseDirectory.value / ".." / "shared" / "src" / "main" / "scala-2.12"
).aggregate(shared).dependsOn(shared).enablePlugins(ScalaJSPlugin, ScalaJSWeb)
val flinkVersion = "1.6.1"
val flinkVersion = "1.7.0"
val flinkDependencies = Seq(
"org.apache.flink" %% "flink-scala" % flinkVersion % "provided",
"org.apache.flink" %% "flink-table" % flinkVersion % "provided",
"org.apache.flink" %% "flink-streaming-scala" % flinkVersion % "provided",
"org.apache.flink" %% "flink-gelly-scala" % "1.6.1")
"org.apache.flink" %% "flink-gelly-scala" % "1.7.0")
lazy val flink = (project in file("flink")).
settings(
scalaVersion := "2.11.12",
scalaVersion := "2.12.8",
resolvers ++= Seq(
"Apache Development Snapshot Repository" at "https://repository.apache.org/content/repositories/snapshots/",
Resolver.mavenLocal
......
# Coupled Sim Apache Flink program
See [../README.md](../README.md)!
......@@ -390,6 +390,8 @@ object CoupledSimulationFlink {
CoupledSimulationFlinkBenchmark.runSizeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation)
} else if (params.has("timemark")) {
CoupledSimulationFlinkBenchmark.runTimeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation)
} else if (params.has("tacasmark")) {
TacasBenchmarks.runTacasMark()
} else {
executeAlgorithm(env,
cfgPath = cfgPath,
......
......@@ -28,7 +28,7 @@ class SignatureRefinement {
val oldSigCount: DataSet[Tuple1[Int]] = coloring.map(_._2).distinct.map(_ => Tuple1(1)).sum(0)
val signatureEdges: DataSet[(Int, (Color, Color))] = ts.getEdgesAsTuple3().join(coloring).where(1).equalTo(0) {
(edge, color) => (edge._1, (edge._3.toInt, color._2))
(edge, color) => (edge._1, (edge._3, color._2))
}
val signatures: DataSet[(Int, Color)] =
signatureEdges.groupBy(0).reduceGroup { g =>
......
package de.bbisping.coupledsim.flink
import org.apache.flink.api.scala.ExecutionEnvironment
import scala.collection.Seq
/**
* Runs the coupled simulation flink algorithm on a number of VLTS samples
* in order to produce the benchmarking results as reported in our TACAS 2019
* paper.
*/
object TacasBenchmarks {
val tacasSamples = Seq(
"shared/src/test/assets/csv/coupled-sim-phil.csv",
"shared/src/test/assets/csv/ltbts.csv",
"shared/src/test/assets/vlts/vasy_0_1.csv", // 289, 1224, no tau, 2
"shared/src/test/assets/vlts/vasy_1_4.csv", // 1183, 4464, 1213, 6
"shared/src/test/assets/vlts/vasy_5_9.csv",
"shared/src/test/assets/vlts/cwi_1_2.csv", // 1952, 2387, 2215, 26
"shared/src/test/assets/vlts/cwi_3_14.csv",// 3996, 14552, 14551, 2
"shared/src/test/assets/vlts/vasy_8_24.csv",
"shared/src/test/assets/vlts/vasy_8_38.csv",
"shared/src/test/assets/vlts/vasy_10_56.csv",
"shared/src/test/assets/vlts/vasy_25_25.csv"
)
val systemPathToTacasHandle = Map(
"shared/src/test/assets/csv/coupled-sim-phil.csv" -> "phil",
"shared/src/test/assets/csv/ltbts.csv" -> "ltbts"
).withDefault(s => s.slice(s.lastIndexOf('/') + 1, s.lastIndexOf('.')))
def runSizeMark(cfgPreminimization: String, cfgOverApproximation: String): Unit = {
val samples = tacasSamples
val env = ExecutionEnvironment.getExecutionEnvironment
env.getConfig.disableSysoutLogging()
for (s <- samples) {
val begin = System.currentTimeMillis()
val csResult = CoupledSimulationFlink.executeAlgorithm(env,
cfgPath = s,
cfgPreminimization = cfgPreminimization,
cfgOverApproximation = cfgOverApproximation,
cfgBenchmarkSizes = true,
cfgReturnPartitionRelation = true)
val time = System.currentTimeMillis() - begin
val benchmark = csResult.benchmarkSizes.withDefaultValue("")
val (csPart, csRel) = csResult.partitionRelation
val csPartitionCount = csPart.values.toSet.size
println(s + ", " +
benchmark("systemStates") + ", " +
benchmark("systemTransitions") + ", " +
benchmark("systemWeakTransitions") + ", " +
benchmark("minimizedStates") + ", " +
benchmark("minimizedTransitions") + ", " +
benchmark("gameNodes") + ", " +
benchmark("gameMoves") + ", " +
csPartitionCount + ", " +
csRel.size + ", " +
time)
}
}
def runTacasMark(): Unit = {
val samples = tacasSamples
val cfgOverApproximation = "bigstep"
val cfgPreminimization = "delaybisim"
val env = ExecutionEnvironment.getExecutionEnvironment
env.getConfig.disableSysoutLogging()
env.setParallelism(4)
println("Warmup for time benchmark using the first four systems...")
for (s <- samples.take(4)) {
val begin = System.currentTimeMillis()
CoupledSimulationFlink.executeAlgorithm(env,
cfgPath = s,
cfgPreminimization = cfgPreminimization,
cfgOverApproximation = cfgOverApproximation)
val time = System.currentTimeMillis() - begin
}
println("\nTime Benchmark\n")
println("system, time/s")
for (s <- samples) {
val begin = System.currentTimeMillis()
CoupledSimulationFlink.executeAlgorithm(env,
cfgPath = s,
cfgPreminimization = cfgPreminimization,
cfgOverApproximation = cfgOverApproximation)
val time = System.currentTimeMillis() - begin
println(systemPathToTacasHandle(s) + ", " + time)
}
println("\nSystem sizes\n")
println("S, ->, =|>, S_DBquotient, >->")
for (s <- samples.dropRight(2)) {
val begin = System.currentTimeMillis()
val csResult = CoupledSimulationFlink.executeAlgorithm(env,
cfgPath = s,
cfgPreminimization = cfgPreminimization,
cfgOverApproximation = "none",
cfgBenchmarkSizes = true,
cfgReturnPartitionRelation = true)
val time = System.currentTimeMillis() - begin
val benchmark = csResult.benchmarkSizes.withDefaultValue("")
println(systemPathToTacasHandle(s) + ", " +
benchmark("systemStates") + ", " +
benchmark("systemTransitions") + ", " +
benchmark("systemWeakTransitions") + ", " +
benchmark("minimizedStates") + ", " +
benchmark("gameMoves"))
}
//vasy_10_56 and vasy_25_25 are omitted as they would crash due to the unoptimized game not
//fitting into the memory.]")
println("vasy_10_56, o.o.m")
println("vasy_25_25, o.o.m")
println("\n>->_sigma, S_CSquotient, CSonQuotient")
for (s <- samples) {
val begin = System.currentTimeMillis()
val csResult = CoupledSimulationFlink.executeAlgorithm(env,
cfgPath = s,
cfgPreminimization = cfgPreminimization,
cfgOverApproximation = cfgOverApproximation,
cfgBenchmarkSizes = true,
cfgReturnPartitionRelation = true)
val time = System.currentTimeMillis() - begin
val benchmark = csResult.benchmarkSizes.withDefaultValue("")
val (csPart, csRel) = csResult.partitionRelation
val csPartitionCount = csPart.values.toSet.size
println(systemPathToTacasHandle(s) + ", " +
benchmark("gameMoves") + ", " +
csPartitionCount + ", " +
csRel.size)
}
}
}
\ No newline at end of file
package de.bbisping.coupledsim.tool
import scala.scalajs.js.JSApp
import scala.scalajs.js.annotation.JSExport
import scala.scalajs.js.annotation.JSExportTopLevel
import de.bbisping.coupledsim.tool.arch.Action
import de.bbisping.coupledsim.tool.arch.ActionDispatcher
import de.bbisping.coupledsim.tool.arch.Control
......@@ -12,7 +12,7 @@ import de.bbisping.coupledsim.tool.view.GraphRenderer
import de.bbisping.coupledsim.tool.view.SourceEditor
import de.bbisping.coupledsim.tool.control.Pipeline
@JSExport
@JSExportTopLevel("TransitionSystemFiddle")
object TransitionSystemFiddle extends JSApp with Control with ActionDispatcher {
val source = new Source(this)
......
......@@ -353,7 +353,7 @@
<script type="text/javascript" src="coupledsim-client-jsdeps.js"></script>
<script type="text/javascript" src="js/cm_transitionsystem_mode.js"></script>
<script type="text/javascript" src="coupledsim-client.js"></script>
<script type="text/javascript">de.bbisping.coupledsim.tool.TransitionSystemFiddle().main();</script>
<script type="text/javascript">TransitionSystemFiddle.main();</script>
</body>
</html>
......@@ -12,74 +12,74 @@ context lts_tau
begin
definition fp_step ::
"'s rel \<Rightarrow> 's rel"
\<open>'s rel \<Rightarrow> 's rel\<close>
where
"fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }"
\<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<Rightarrow>^a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }\<close>
lemma mono_fp_step:
"mono fp_step"
\<open>mono fp_step\<close>
proof (rule, safe)
fix x y::"'s rel" and p q
fix x y::\<open>'s rel\<close> and p q
assume
"x \<subseteq> y"
"(p, q) \<in> fp_step x"
thus "(p, q) \<in> fp_step y"
\<open>x \<subseteq> y\<close>
\<open>(p, q) \<in> fp_step x\<close>
thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def
by (auto, blast)
qed
lemma fp_fp_step:
assumes
"R = fp_step R"
\<open>R = fp_step R\<close>
shows
"coupled_simulation (\<lambda> p q. (p, q) \<in> R)"
\<open>coupled_simulation (\<lambda> p q. (p, q) \<in> R)\<close>
using assms unfolding fp_step_def coupled_simulation_def
by fastforce
lemma gfp_fp_step_subset_gcs:
shows "(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }"
shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify
fix a b
assume
"(a, b) \<in> gfp fp_step"
thus "a \<sqsubseteq>cs b"
\<open>(a, b) \<in> gfp fp_step\<close>
thus \<open>a \<sqsubseteq>cs b\<close>
using fp_fp_step mono_fp_step gfp_unfold by auto
qed
lemma fp_fp_step_gcs:
assumes
"R = { (p,q) . greatest_coupled_simulation p q }"
\<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows
"fp_step R = R"
\<open>fp_step R = R\<close>
unfolding assms
proof safe
fix p q
assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
\<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
hence \<open>(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
unfolding fp_step_def by auto
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)" using weak_step_tau2_def by simp
thus "greatest_coupled_simulation p q"
hence \<open>(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close> using weak_step_tau2_def by simp
thus \<open>greatest_coupled_simulation p q\<close>
using lts_tau.gcs by metis
next
fix p q
assume
"greatest_coupled_simulation p q"
hence "(p, q) \<in> {(x, y). greatest_coupled_simulation x y} \<and> (\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q \<longmapsto>^ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))"
\<open>greatest_coupled_simulation p q\<close>
hence \<open>(p, q) \<in> {(x, y). greatest_coupled_simulation x y} \<and> (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q \<Rightarrow>^a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))\<close>
using gcs_is_coupled_simulation unfolding coupled_simulation_def by blast
thus "(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
thus \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
unfolding fp_step_def by blast
qed
lemma gfp_fp_step_gcs: "gfp fp_step = { (p,q) . greatest_coupled_simulation p q }"
lemma gfp_fp_step_gcs: \<open>gfp fp_step = { (p,q) . greatest_coupled_simulation p q }\<close>
using fp_fp_step_gcs gfp_fp_step_subset_gcs
by (simp add: equalityI gfp_upperbound)
......@@ -89,11 +89,11 @@ context lts_tau_finite
begin
lemma gfp_fp_step_while:
shows
"gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top"
\<open>gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top\<close>
using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast
theorem coupled_sim_fp_step_while:
shows "while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }"
shows \<open>while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }\<close>
using gfp_fp_step_while gfp_fp_step_gcs by blast
end
......
section \<open>Fixed Point Algorithm for Coupled Similarity\<close>
subsection \<open>The Algorithm\<close>
theory CS_Fixpoint_Algo_Delay
imports
Coupled_Simulation
Finite_Weak_Transition_Systems
"~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Finite_Lattice"
begin
......@@ -12,83 +14,99 @@ context lts_tau
begin
definition fp_step ::
"'s rel \<Rightarrow> 's rel"
where
"fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^~ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }"
\<open>'s rel \<Rightarrow> 's rel\<close>
where
\<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(tau a \<longrightarrow> (p',q)\<in>R1) \<and>
(\<not>tau a \<longrightarrow> (\<exists> q'. ((p',q')\<in>R1) \<and> (q =\<rhd>a q')))) \<and>
(\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }\<close>
definition fp_compute_cs :: \<open>'s rel\<close>
where \<open>fp_compute_cs \<equiv> while (\<lambda>R. fp_step R \<noteq> R) fp_step top\<close>
subsection \<open>Correctness\<close>
lemma mono_fp_step:
"mono fp_step"
\<open>mono fp_step\<close>
proof (rule, safe)
fix x y::"'s rel" and p q
fix x y::\<open>'s rel\<close> and p q
assume
"x \<subseteq> y"
"(p, q) \<in> fp_step x"
thus "(p, q) \<in> fp_step y"
\<open>x \<subseteq> y\<close>
\<open>(p, q) \<in> fp_step x\<close>
thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def
by (auto, blast)
qed
thm prod.simps(2)
lemma fp_fp_step:
assumes
"R = fp_step R"
\<open>R = fp_step R\<close>
shows
"coupled_delay_simulation (\<lambda> p q. (p, q) \<in> R)"
\<open>coupled_delay_simulation (\<lambda> p q. (p, q) \<in> R)\<close>
using assms unfolding fp_step_def coupled_delay_simulation_def delay_simulation_def
by fastforce
by (auto, blast, fastforce+)
lemma gfp_fp_step_subset_gcs:
shows "(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }"
shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify
fix a b
assume
"(a, b) \<in> gfp fp_step"
thus "a \<sqsubseteq>cs b"
unfolding coupled_sim_by_eq_delay_coupled_simulation
\<open>(a, b) \<in> gfp fp_step\<close>
thus \<open>a \<sqsubseteq>cs b\<close>
unfolding coupled_sim_by_eq_coupled_delay_simulation
using fp_fp_step mono_fp_step gfp_unfold
by metis
qed
lemma fp_fp_step_gcs:
assumes
"R = { (p,q) . greatest_coupled_simulation p q }"
\<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows
"fp_step R = R"
\<open>fp_step R = R\<close>
unfolding assms
proof safe
fix p q
assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^~ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
\<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
hence
\<open>(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow>
(tau a \<longrightarrow> greatest_coupled_simulation p' q) \<and>
(\<not>tau a \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q =\<rhd>a q'))) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
unfolding fp_step_def by auto
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
unfolding fp_step_def using weak_step_delay_implies_weak_tau by blast
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)" using weak_step_tau2_def by simp
thus "greatest_coupled_simulation p q"
hence \<open>(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
unfolding fp_step_def using weak_step_delay_implies_weak_tau steps.refl by blast
hence \<open>(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^^a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
using weak_step_tau2_def by simp
thus \<open>greatest_coupled_simulation p q\<close>
using lts_tau.gcs by metis
next
fix p q
assume asm:
"greatest_coupled_simulation p q"
then have "(p, q) \<in> {(x, y). greatest_coupled_simulation x y}" by blast
\<open>greatest_coupled_simulation p q\<close>
then have \<open>(p, q) \<in> {(x, y). greatest_coupled_simulation x y}\<close> by blast
moreover from asm have \<open>\<exists> R. R p q \<and> coupled_delay_simulation R\<close>
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_delay_coupled_simulation .
moreover from asm have "(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> (\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q \<longmapsto>^~ a q')))"