...
 
Commits (7)
......@@ -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)"
using assms unfolding fp_step_def coupled_delay_simulation_def delay_simulation_def
by fastforce
\<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 (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')))"
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_delay_coupled_simulation
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation .
moreover from asm have \<open>\<forall> p' a. p \<longmapsto>a p' \<and> \<not>tau a \<longrightarrow>
(\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q =\<rhd>a q'))\<close>
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation
by (metis coupled_delay_simulation_def delay_simulation_def)
moreover from asm have \<open>\<forall> p' a. p \<longmapsto>a p' \<and> tau a \<longrightarrow> greatest_coupled_simulation p' q\<close>
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation
by (metis coupled_delay_simulation_def delay_simulation_def)
moreover have "(\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))"
moreover have \<open>(\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))\<close>
using asm gcs_is_coupled_simulation coupled_simulation_implies_coupling by blast
ultimately show "(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
ultimately show \<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)
......@@ -98,14 +116,14 @@ 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 = fp_compute_cs\<close>
unfolding fp_compute_cs_def
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>fp_compute_cs = { (p,q) . greatest_coupled_simulation p q }\<close>
using gfp_fp_step_while gfp_fp_step_gcs by blast
end
end
......@@ -14,258 +14,258 @@ datatype ('s, 'a) cs_game_node =
DefenderCouplingNode 's 's
fun (in lts_tau) cs_game_moves ::
"('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool" where
\<open>('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
simulation_challenge:
"cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
(p \<longmapsto> a p1 \<and> q = q0)" |
\<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
(p \<longmapsto>a p1 \<and> q = q0)\<close> |
simulation_answer:
"cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =
(q0 \<longmapsto>^ a q1 \<and> p1 = p11)" |
\<open>cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =
(q0 \<Rightarrow>^a q1 \<and> p1 = p11)\<close> |
coupling_challenge:
"cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
(p = p0 \<and> q = q0)" |
\<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
(p = p0 \<and> q = q0)\<close> |
coupling_answer:
"cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
(p0 = p00 \<and> q0 \<longmapsto>* tau q1)" |
\<open>cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
(p0 = p00 \<and> q0 \<longmapsto>* tau q1)\<close> |
cs_game_moves_no_step:
"cs_game_moves _ _ = False"
\<open>cs_game_moves _ _ = False\<close>
fun cs_game_defender_node :: "('s, 'a) cs_game_node \<Rightarrow> bool" where
"cs_game_defender_node (AttackerNode _ _) = False" |
"cs_game_defender_node (DefenderStepNode _ _ _) = True" |
"cs_game_defender_node (DefenderCouplingNode _ _) = True"
fun cs_game_defender_node :: \<open>('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
\<open>cs_game_defender_node (AttackerNode _ _) = False\<close> |
\<open>cs_game_defender_node (DefenderStepNode _ _ _) = True\<close> |
\<open>cs_game_defender_node (DefenderCouplingNode _ _) = True\<close>
locale cs_game =
lts_tau trans \<tau> +
simple_game cs_game_moves cs_game_defender_node initial
for
trans :: "'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" and
\<tau> :: "'a" and
initial :: "('s, 'a) cs_game_node"
trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close> and
\<tau> :: \<open>'a\<close> and
initial :: \<open>('s, 'a) cs_game_node\<close>
begin
subsection \<open>Coupled Simulation Implies Winning Strategy\<close>
fun strategy_from_coupledsim :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) cs_game_node strategy" where
"strategy_from_coupledsim R ((DefenderStepNode a p1 q0)#play) =
(AttackerNode p1 (SOME q1 . R p1 q1 \<and> q0 \<longmapsto>^ a q1))" |
"strategy_from_coupledsim R ((DefenderCouplingNode p0 q0)#play) =
(AttackerNode (SOME q1 . R q1 p0 \<and> q0 \<longmapsto>* tau q1) p0)" |
"strategy_from_coupledsim _ _ = undefined"
fun strategy_from_coupledsim :: \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) cs_game_node strategy\<close> where
\<open>strategy_from_coupledsim R ((DefenderStepNode a p1 q0)#play) =
(AttackerNode p1 (SOME q1 . R p1 q1 \<and> q0 \<Rightarrow>^a q1))\<close> |
\<open>strategy_from_coupledsim R ((DefenderCouplingNode p0 q0)#play) =
(AttackerNode (SOME q1 . R q1 p0 \<and> q0 \<longmapsto>* tau q1) p0)\<close> |
\<open>strategy_from_coupledsim _ _ = undefined\<close>
lemma attacker_followed_by_defender:
lemma defender_preceded_by_attacker:
assumes
"n0 # play \<in> plays"
"cs_game_defender_node n0"
"initial = AttackerNode p0 q0"
shows "\<exists> p q . hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0" "play \<noteq> []"
\<open>n0 # play \<in> plays\<close>
\<open>cs_game_defender_node n0\<close>
\<open>initial = AttackerNode p0 q0\<close>
shows \<open>\<exists> p q . hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> \<open>play \<noteq> []\<close>
proof -
have n0_not_init: "n0 \<noteq> initial" using assms(2,3) by auto
hence "cs_game_moves (hd play) n0" using assms(1)
have n0_not_init: \<open>n0 \<noteq> initial\<close> using assms(2,3) by auto
hence \<open>cs_game_moves (hd play) n0\<close> using assms(1)
by (metis list.sel(1) list.sel(3) plays.cases)
thus "\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0" using assms(2)
thus \<open>\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> using assms(2)
by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,7))
show "play \<noteq> []" using n0_not_init assms(1) plays.cases by auto
show \<open>play \<noteq> []\<close> using n0_not_init assms(1) plays.cases by auto
qed
lemma strategy_from_coupledsim_retains_coupledsim:
assumes
"R p0 q0"
"coupled_simulation R"
"initial = AttackerNode p0 q0"
"play \<in> plays_for_strategy (strategy_from_coupledsim R)"
\<open>R p0 q0\<close>
\<open>coupled_simulation R\<close>
\<open>initial = AttackerNode p0 q0\<close>
\<open>play \<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
shows
"hd play = AttackerNode p q \<Longrightarrow> R p q"
"length play > 1 \<Longrightarrow> hd (tl play) = AttackerNode p q \<Longrightarrow> R p q"
\<open>hd play = AttackerNode p q \<Longrightarrow> R p q\<close>
\<open>length play > 1 \<Longrightarrow> hd (tl play) = AttackerNode p q \<Longrightarrow> R p q\<close>
using assms(4)
proof (induct arbitrary: p q rule: plays_for_strategy.induct[OF assms(4)])
case 1
fix p q
assume "hd [initial] = AttackerNode p q"
hence "p = p0" "q = q0" using assms(3) by auto
thus "R p q" using assms(1) by simp
assume \<open>hd [initial] = AttackerNode p q\<close>
hence \<open>p = p0\<close> \<open>q = q0\<close> using assms(3) by auto
thus \<open>R p q\<close> using assms(1) by simp
next
case 1
fix p q
assume "1 < length [initial]"
assume \<open>1 < length [initial]\<close>
hence False by auto
thus "R p q" ..
thus \<open>R p q\<close> ..
next
case (2 n0 play)
hence n0play_is_play: "n0 # play \<in> plays" using strategy_plays_subset by blast
hence n0play_is_play: \<open>n0 # play \<in> plays\<close> using strategy_plays_subset by blast
fix p q
assume subassms:
"hd (strategy_from_coupledsim R (n0 # play) # n0 # play) = AttackerNode p q"
"strategy_from_coupledsim R (n0 # play) # n0 # play
\<in> plays_for_strategy (strategy_from_coupledsim R)"
\<open>hd (strategy_from_coupledsim R (n0 # play) # n0 # play) = AttackerNode p q\<close>
\<open>strategy_from_coupledsim R (n0 # play) # n0 # play
\<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
then obtain pi qi where
piqi_def: "hd (play) = AttackerNode pi qi"
"cs_game_moves (AttackerNode pi qi) n0" "play \<noteq> []"
using attacker_followed_by_defender[OF n0play_is_play `cs_game_defender_node n0` assms(3)]
piqi_def: \<open>hd (play) = AttackerNode pi qi\<close>
\<open>cs_game_moves (AttackerNode pi qi) n0\<close> \<open>play \<noteq> []\<close>
using defender_preceded_by_attacker[OF n0play_is_play `cs_game_defender_node n0` assms(3)]
by blast
hence "R pi qi" using 2(1,3) by simp
have "(\<exists> a . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto> a p)
\<or> (n0 = (DefenderCouplingNode pi qi))"
hence \<open>R pi qi\<close> using 2(1,3) by simp
have \<open>(\<exists> a . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto>a p)
\<or> (n0 = (DefenderCouplingNode pi qi))\<close>
using piqi_def(2) 2(4,5) subassms(1)
by (metis cs_game_defender_node.elims(2) cs_game_moves.simps(2) list.sel(1)
coupling_challenge simulation_challenge)
thus "R p q"
thus \<open>R p q\<close>
proof safe
fix a
assume n0_def: "n0 = DefenderStepNode a p qi" "pi \<longmapsto>a p"
have "strategy_from_coupledsim R (n0 # play) =
(AttackerNode p (SOME q1 . R p q1 \<and> qi \<longmapsto>^ a q1))"
assume n0_def: \<open>n0 = DefenderStepNode a p qi\<close> \<open>pi \<longmapsto>a p\<close>
have \<open>strategy_from_coupledsim R (n0 # play) =
(AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1))\<close>
unfolding n0_def(1) by auto
with subassms(1) have q_def: "q = (SOME q1. R p q1 \<and> qi \<longmapsto>^ a q1)" by auto
have "\<exists> qii . R p qii \<and> qi \<longmapsto>^ a qii"
with subassms(1) have q_def: \<open>q = (SOME q1. R p q1 \<and> qi \<Rightarrow>^a q1)\<close> by auto
have \<open>\<exists> qii . R p qii \<and> qi \<Rightarrow>^a qii\<close>
using n0_def(2) `R pi qi` `coupled_simulation R`
unfolding coupled_simulation_def by blast
from someI_ex[OF this] show "R p q" unfolding q_def by blast
from someI_ex[OF this] show \<open>R p q\<close> unfolding q_def by blast
next
assume n0_def: "n0 = DefenderCouplingNode pi qi"
have "strategy_from_coupledsim R (n0 # play) =
(AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi)"
assume n0_def: \<open>n0 = DefenderCouplingNode pi qi\<close>
have \<open>strategy_from_coupledsim R (n0 # play) =
(AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi)\<close>
unfolding n0_def(1) by auto
with subassms(1) have qp_def: "p = (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1)" "q = pi" by auto
have "\<exists> q1 . R q1 pi \<and> qi \<longmapsto>* tau q1"
with subassms(1) have qp_def: \<open>p = (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1)\<close> \<open>q = pi\<close> by auto
have \<open>\<exists> q1 . R q1 pi \<and> qi \<longmapsto>* tau q1\<close>
using n0_def `R pi qi` `coupled_simulation R`
unfolding coupled_simulation_def by blast
from someI_ex[OF this] show "R p q" unfolding qp_def by blast
from someI_ex[OF this] show \<open>R p q\<close> unfolding qp_def by blast
qed
next
case (2 n0 play)
fix p q
assume "hd (tl (strategy_from_coupledsim R (n0 # play) # n0 # play)) = AttackerNode p q"
assume \<open>hd (tl (strategy_from_coupledsim R (n0 # play) # n0 # play)) = AttackerNode p q\<close>
hence False using 2(4) by auto
thus "R p q" ..
thus \<open>R p q\<close> ..
next
case (3 n1 play n1')
fix p q
assume "hd (n1' # n1 # play) = AttackerNode p q"
assume \<open>hd (n1' # n1 # play) = AttackerNode p q\<close>
hence False using 3(4,5) unfolding player1_position_def
by (metis cs_game_moves_no_step(5) cs_game_defender_node.elims(3) list.sel(1))
thus "R p q" ..
thus \<open>R p q\<close> ..
next
case (3 n1 play n1')
fix p q
assume "hd (tl (n1' # n1 # play)) = AttackerNode p q"
thus "R p q" using 3(1,2) by auto
assume \<open>hd (tl (n1' # n1 # play)) = AttackerNode p q\<close>
thus \<open>R p q\<close> using 3(1,2) by auto
qed
lemma strategy_from_coupledsim_sound:
assumes
"R p0 q0"
"coupled_simulation R"
"initial = AttackerNode p0 q0"
\<open>R p0 q0\<close>
\<open>coupled_simulation R\<close>
\<open>initial = AttackerNode p0 q0\<close>
shows
"sound_strategy (strategy_from_coupledsim R)"
\<open>sound_strategy (strategy_from_coupledsim R)\<close>
unfolding sound_strategy_def
proof clarify
fix n0 play
assume subassms:
"n0 # play \<in> plays_for_strategy(strategy_from_coupledsim R)"
"cs_game_defender_node n0"
\<open>n0 # play \<in> plays_for_strategy(strategy_from_coupledsim R)\<close>
\<open>cs_game_defender_node n0\<close>
then obtain pi qi where
piqi_def: "hd (play) = AttackerNode pi qi"
"cs_game_moves (AttackerNode pi qi) n0" "play \<noteq> []"
using attacker_followed_by_defender[OF _ `cs_game_defender_node n0` assms(3)]
piqi_def: \<open>hd (play) = AttackerNode pi qi\<close>
\<open>cs_game_moves (AttackerNode pi qi) n0\<close> \<open>play \<noteq> []\<close>
using defender_preceded_by_attacker[OF _ `cs_game_defender_node n0` assms(3)]
strategy_plays_subset by blast
hence "R pi qi"
hence \<open>R pi qi\<close>
using strategy_from_coupledsim_retains_coupledsim[OF assms] list.sel subassms by auto
have "(\<exists> a p . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto> a p)
\<or> (n0 = (DefenderCouplingNode pi qi))"
have \<open>(\<exists> a p . n0 = (DefenderStepNode a p qi) \<and> pi \<longmapsto>a p)
\<or> (n0 = (DefenderCouplingNode pi qi))\<close>
by (metis cs_game_defender_node.elims(2)
coupling_challenge simulation_challenge piqi_def(2) subassms(2))
thus "cs_game_moves n0 (strategy_from_coupledsim R (n0 # play))"
thus \<open>cs_game_moves n0 (strategy_from_coupledsim R (n0 # play))\<close>
proof safe
fix a p
assume dsn:
"pi \<longmapsto>a p"
"n0 = DefenderStepNode a p qi"
\<open>pi \<longmapsto>a p\<close>
\<open>n0 = DefenderStepNode a p qi\<close>
hence qi_spec:
"(strategy_from_coupledsim R (n0 # play)) =
AttackerNode p (SOME q1 . R p q1 \<and> qi \<longmapsto>^ a q1)"
\<open>(strategy_from_coupledsim R (n0 # play)) =
AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1)\<close>
by simp
then obtain qii where qii_spec:
"AttackerNode p (SOME q1 . R p q1 \<and> qi \<longmapsto>^ a q1) = AttackerNode p qii" by blast
have "\<exists> qii . R p qii \<and> qi \<longmapsto>^ a qii"
\<open>AttackerNode p (SOME q1 . R p q1 \<and> qi \<Rightarrow>^a q1) = AttackerNode p qii\<close> by blast
have \<open>\<exists> qii . R p qii \<and> qi \<Rightarrow>^a qii\<close>
using dsn `R pi qi` `coupled_simulation R`
unfolding coupled_simulation_def by blast
from someI_ex[OF this] have "R p qii \<and> qi \<longmapsto>^ a qii" using qii_spec by blast
thus "cs_game_moves (DefenderStepNode a p qi)
(strategy_from_coupledsim R (DefenderStepNode a p qi # play))"
from someI_ex[OF this] have \<open>R p qii \<and> qi \<Rightarrow>^a qii\<close> using qii_spec by blast
thus \<open>cs_game_moves (DefenderStepNode a p qi)
(strategy_from_coupledsim R (DefenderStepNode a p qi # play))\<close>
using qi_spec qii_spec unfolding dsn(2) by auto
next \<comment>\<open>coupling quite analogous.\<close>
assume dcn:
"n0 = DefenderCouplingNode pi qi"
\<open>n0 = DefenderCouplingNode pi qi\<close>
hence qi_spec:
"(strategy_from_coupledsim R (n0 # play)) =
AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi"
\<open>(strategy_from_coupledsim R (n0 # play)) =
AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi\<close>
by simp
then obtain qii where qii_spec:
"AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi = AttackerNode qii pi" by blast
have "\<exists> qii . R qii pi \<and> qi \<longmapsto>* tau qii"
\<open>AttackerNode (SOME q1 . R q1 pi \<and> qi \<longmapsto>* tau q1) pi = AttackerNode qii pi\<close> by blast
have \<open>\<exists> qii . R qii pi \<and> qi \<longmapsto>* tau qii\<close>
using dcn `R pi qi` `coupled_simulation R`
unfolding coupled_simulation_def by blast
from someI_ex[OF this] have "R qii pi \<and> qi \<longmapsto>* tau qii" using qii_spec by blast
thus "cs_game_moves (DefenderCouplingNode pi qi)
(strategy_from_coupledsim R (DefenderCouplingNode pi qi # play))"
from someI_ex[OF this] have \<open>R qii pi \<and> qi \<longmapsto>* tau qii\<close> using qii_spec by blast
thus \<open>cs_game_moves (DefenderCouplingNode pi qi)
(strategy_from_coupledsim R (DefenderCouplingNode pi qi # play))\<close>
using qi_spec qii_spec unfolding dcn by auto
qed
qed
lemma coupledsim_implies_winning_strategy:
assumes
"R p q"
"coupled_simulation R"
"initial = AttackerNode p q"
\<open>R p q\<close>
\<open>coupled_simulation R\<close>
\<open>initial = AttackerNode p q\<close>
shows
"player0_winning_strategy (strategy_from_coupledsim R)"
\<open>player0_winning_strategy (strategy_from_coupledsim R)\<close>
unfolding player0_winning_strategy_def
proof (clarify)
fix play
assume subassms:
"play \<in> plays_for_strategy (strategy_from_coupledsim R)"
"player1_wins play"
show "False" using subassms
\<open>play \<in> plays_for_strategy (strategy_from_coupledsim R)\<close>
\<open>player1_wins play\<close>
show \<open>False\<close> using subassms
proof (induct rule: simple_game.plays_for_strategy.induct[OF subassms(1)])
case 1
then show ?case unfolding player1_wins_def using assms(3) by auto
next
case (2 n0 play)
hence "\<not> cs_game_defender_node (strategy_from_coupledsim R (n0 # play))"
hence \<open>\<not> cs_game_defender_node (strategy_from_coupledsim R (n0 # play))\<close>
using cs_game_moves_no_step cs_game_defender_node.elims(2) by metis
hence "\<not> player1_wins (strategy_from_coupledsim R (n0 # play) # n0 # play)"
hence \<open>\<not> player1_wins (strategy_from_coupledsim R (n0 # play) # n0 # play)\<close>
unfolding player1_wins_def by auto
thus ?case using 2(6) by auto
next
case (3 n1 play n1')
then obtain p q where n1_def: "n1 = AttackerNode p q"
then obtain p q where n1_def: \<open>n1 = AttackerNode p q\<close>
unfolding player1_position_def using cs_game_defender_node.elims(3) by blast
hence "R p q"
using strategy_from_coupledsim_retains_coupledsim[OF assms, of "n1 # play"] 3(1) by auto
have "(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto> a p1))
\<or> n1' = (DefenderCouplingNode p q)"
hence \<open>R p q\<close>
using strategy_from_coupledsim_retains_coupledsim[OF assms, of \<open>n1 # play\<close>] 3(1) by auto
have \<open>(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto>a p1))
\<or> n1' = (DefenderCouplingNode p q)\<close>
using n1_def `cs_game_moves n1 n1'` coupling_challenge cs_game_moves_no_step(5)
simulation_challenge
by (metis cs_game_defender_node.elims(2, 3))
then show ?case
proof
assume "(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto> a p1))"
assume \<open>(\<exists> p1 a . n1' = (DefenderStepNode a p1 q) \<and> (p \<longmapsto>a p1))\<close>
then obtain p1 a where
n1'_def: "n1' = (DefenderStepNode a p1 q)" "p \<longmapsto> a p1"
n1'_def: \<open>n1' = (DefenderStepNode a p1 q)\<close> \<open>p \<longmapsto>a p1\<close>
by blast
hence "\<exists> q1 . q \<longmapsto>^ a q1"
hence \<open>\<exists> q1 . q \<Rightarrow>^a q1\<close>
using `R p q` `coupled_simulation R` unfolding coupled_simulation_def by blast
hence "\<exists> q1 . cs_game_moves (DefenderStepNode a p1 q) (AttackerNode p1 q1)"
hence \<open>\<exists> q1 . cs_game_moves (DefenderStepNode a p1 q) (AttackerNode p1 q1)\<close>
by auto
with `player1_wins (n1' # n1 # play)` show False unfolding player1_wins_def n1'_def
by (metis list.sel(1))
next
assume n1'_def: "n1' = DefenderCouplingNode p q"
have "\<exists> q1 . q \<longmapsto>*tau q1"
assume n1'_def: \<open>n1' = DefenderCouplingNode p q\<close>
have \<open>\<exists> q1 . q \<longmapsto>*tau q1\<close>
using `coupled_simulation R` `R p q` unfolding coupled_simulation_def by blast
hence "\<exists> q1 . cs_game_moves (DefenderCouplingNode p q) (AttackerNode q1 p)"
hence \<open>\<exists> q1 . cs_game_moves (DefenderCouplingNode p q) (AttackerNode q1 p)\<close>
by auto
with `player1_wins (n1' # n1 # play)` show False unfolding player1_wins_def n1'_def
by (metis list.sel(1))
......@@ -277,89 +277,89 @@ subsection \<open>Winning Strategy Induces Coupled Simulation\<close>
lemma winning_strategy_implies_coupledsim:
assumes
"player0_winning_strategy f"
"sound_strategy f"
\<open>player0_winning_strategy f\<close>
\<open>sound_strategy f\<close>
defines
"R == \<lambda> p q . (\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)"
\<open>R == \<lambda> p q . (\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
shows
"coupled_simulation R"
\<open>coupled_simulation R\<close>
unfolding coupled_simulation_def
proof safe
fix p q p' a
assume challenge:
"R p q"
"p \<longmapsto>a p'"
hence game_move: "cs_game_moves (AttackerNode p q) (DefenderStepNode a p' q)" by auto
have "(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)"
\<open>R p q\<close>
\<open>p \<longmapsto>a p'\<close>
hence game_move: \<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p' q)\<close> by auto
have \<open>(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
using challenge(1) assms by blast
then obtain play where
play_spec: "AttackerNode p q # play \<in> plays_for_strategy f"
play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
hence interplay: "(DefenderStepNode a p' q) # AttackerNode p q # play \<in> plays_for_strategy f"
hence interplay: \<open>(DefenderStepNode a p' q) # AttackerNode p q # play \<in> plays_for_strategy f\<close>
using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
hence "\<not> player1_wins ((DefenderStepNode a p' q) # AttackerNode p q # play)"
hence \<open>\<not> player1_wins ((DefenderStepNode a p' q) # AttackerNode p q # play)\<close>
using assms(1) unfolding player0_winning_strategy_def by blast
then obtain n1 where n1_def:
"n1 = f (DefenderStepNode a p' q # AttackerNode p q # play)"
"cs_game_moves (DefenderStepNode a p' q) n1"
\<open>n1 = f (DefenderStepNode a p' q # AttackerNode p q # play)\<close>
\<open>cs_game_moves (DefenderStepNode a p' q) n1\<close>
using interplay assms(2) unfolding player0_winning_strategy_def sound_strategy_def by simp
obtain q' where q'_spec:
"(AttackerNode p' q') = n1" "q \<longmapsto>^ a q'"
\<open>(AttackerNode p' q') = n1\<close> \<open>q \<Rightarrow>^a q'\<close>
using n1_def(2) by (cases n1, auto)
hence "(AttackerNode p' q') # (DefenderStepNode a p' q) # AttackerNode p q # play
\<in> plays_for_strategy f"
hence \<open>(AttackerNode p' q') # (DefenderStepNode a p' q) # AttackerNode p q # play
\<in> plays_for_strategy f\<close>
using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
hence "R p' q'" unfolding R_def by (meson list.sel(1))
thus "\<exists>q'. R p' q' \<and> q \<longmapsto>^ a q'" using q'_spec(2) by blast
hence \<open>R p' q'\<close> unfolding R_def by (meson list.sel(1))
thus \<open>\<exists>q'. R p' q' \<and> q \<Rightarrow>^a q'\<close> using q'_spec(2) by blast
next
fix p q
assume challenge:
"R p q"
hence game_move: "cs_game_moves (AttackerNode p q) (DefenderCouplingNode p q)" by auto
have "(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)"
\<open>R p q\<close>
hence game_move: \<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p q)\<close> by auto
have \<open>(\<exists> play \<in> plays_for_strategy f . hd play = AttackerNode p q)\<close>
using challenge assms by blast
then obtain play where
play_spec: "AttackerNode p q # play \<in> plays_for_strategy f"
play_spec: \<open>AttackerNode p q # play \<in> plays_for_strategy f\<close>
by (metis list.sel(1) simple_game.plays.cases strategy_plays_subset)
hence interplay: "(DefenderCouplingNode p q) # AttackerNode p q # play
\<in> plays_for_strategy f"
hence interplay: \<open>(DefenderCouplingNode p q) # AttackerNode p q # play
\<in> plays_for_strategy f\<close>
using game_move by (simp add: player1_position_def simple_game.plays_for_strategy.p1move)
hence "\<not> player1_wins ((DefenderCouplingNode p q) # AttackerNode p q # play)"
hence \<open>\<not> player1_wins ((DefenderCouplingNode p q) # AttackerNode p q # play)\<close>
using assms(1) unfolding player0_winning_strategy_def by blast
then obtain n1 where n1_def:
"n1 = f (DefenderCouplingNode p q # AttackerNode p q # play)"
"cs_game_moves (DefenderCouplingNode p q) n1"
\<open>n1 = f (DefenderCouplingNode p q # AttackerNode p q # play)\<close>
\<open>cs_game_moves (DefenderCouplingNode p q) n1\<close>
using interplay assms(2)
unfolding player0_winning_strategy_def sound_strategy_def by simp
obtain q' where q'_spec:
"(AttackerNode q' p) = n1" "q \<longmapsto>* tau q'"
\<open>(AttackerNode q' p) = n1\<close> \<open>q \<longmapsto>* tau q'\<close>
using n1_def(2) by (cases n1, auto)
hence "(AttackerNode q' p) # (DefenderCouplingNode p q) # AttackerNode p q # play
\<in> plays_for_strategy f"
hence \<open>(AttackerNode q' p) # (DefenderCouplingNode p q) # AttackerNode p q # play
\<in> plays_for_strategy f\<close>
using interplay n1_def by (simp add: simple_game.plays_for_strategy.p0move)
hence "R q' p" unfolding R_def by (meson list.sel(1))
thus "\<exists>q'. q \<longmapsto>* tau q' \<and> R q' p" using q'_spec(2) by blast
hence \<open>R q' p\<close> unfolding R_def by (meson list.sel(1))
thus \<open>\<exists>q'. q \<longmapsto>* tau q' \<and> R q' p\<close> using q'_spec(2) by blast
qed
theorem winning_strategy_iff_coupledsim:
assumes
"initial = AttackerNode p q"
\<open>initial = AttackerNode p q\<close>
shows
"(\<exists> f . player0_winning_strategy f \<and> sound_strategy f)
= p \<sqsubseteq>cs q"
\<open>(\<exists> f . player0_winning_strategy f \<and> sound_strategy f)
= p \<sqsubseteq>cs q\<close>
proof (rule)
assume
"(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)"
\<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
then obtain f where
"coupled_simulation (\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q)"
\<open>coupled_simulation (\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q)\<close>
using winning_strategy_implies_coupledsim by blast
moreover have "(\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q) p q"
moreover have \<open>(\<lambda>p q. \<exists>play\<in>plays_for_strategy f. hd play = AttackerNode p q) p q\<close>
using assms plays_for_strategy.init[of f] by (meson list.sel(1))
ultimately show "p \<sqsubseteq>cs q" by blast
ultimately show \<open>p \<sqsubseteq>cs q\<close> by blast
next
assume
"p \<sqsubseteq>cs q"
thus "(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)"
\<open>p \<sqsubseteq>cs q\<close>
thus \<open>(\<exists>f. player0_winning_strategy f \<and> sound_strategy f)\<close>
using coupledsim_implies_winning_strategy[OF _ _ assms]
strategy_from_coupledsim_sound[OF _ _ assms] by blast
qed
......
......@@ -14,260 +14,277 @@ datatype ('s, 'a) cs_game_node =
DefenderCouplingNode 's 's
fun (in lts_tau) cs_game_moves ::
"('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool" where
simulation_challenge:
"cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
(p \<longmapsto> a p1 \<and> q = q0)" |
simulation_answer:
"cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =
(q0 \<longmapsto>^~ a q1 \<and> p1 = p11)" |
coupling_challenge:\<comment>\<open>only difference for delay!\<close>
"cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
(p = p0 \<and> q = q0)" |
\<open>('s, 'a) cs_game_node \<Rightarrow> ('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
simulation_visible_challenge:
\<open>cs_game_moves (AttackerNode p q) (DefenderStepNode a p1 q0) =
(\<not>tau a \<and> p \<longmapsto>a p1 \<and> q = q0)\<close> |
simulation_internal_attacker_move:
\<open>cs_game_moves (AttackerNode p q) (AttackerNode p1 q0) =
(\<exists>a. tau a \<and> p \<longmapsto>a p1 \<and> q = q0)\<close> |
simulation_answer:
\<open>cs_game_moves (DefenderStepNode a p1 q0) (AttackerNode p11 q1) =
(q0 =\<rhd>a q1 \<and> p1 = p11)\<close> |
coupling_challenge:
\<open>cs_game_moves (AttackerNode p q) (DefenderCouplingNode p0 q0) =
(p = p0 \<and> q = q0)\<close> |
coupling_answer:
"cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
(p0 = p00 \<and> q0 \<longmapsto>* tau q1)" |
\<open>cs_game_moves (DefenderCouplingNode p0 q0) (AttackerNode q1 p00) =
(p0 = p00 \<and> q0 \<longmapsto>* tau q1)\<close> |
cs_game_moves_no_step:
"cs_game_moves _ _ = False"
\<open>cs_game_moves _ _ = False\<close>
fun cs_game_defender_node :: "('s, 'a) cs_game_node \<Rightarrow> bool" where
"cs_game_defender_node (AttackerNode _ _) = False" |
"cs_game_defender_node (DefenderStepNode _ _ _) = True" |
"cs_game_defender_node (DefenderCouplingNode _ _) = True"
fun cs_game_defender_node :: \<open>('s, 'a) cs_game_node \<Rightarrow> bool\<close> where
\<open>cs_game_defender_node (AttackerNode _ _) = False\<close> |
\<open>cs_game_defender_node (DefenderStepNode _ _ _) = True\<close> |
\<open>cs_game_defender_node (DefenderCouplingNode _ _) = True\<close>
locale cs_game =
lts_tau trans \<tau> +
simple_game cs_game_moves cs_game_defender_node initial
for
trans :: "'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" and
\<tau> :: "'a" and
initial :: "('s, 'a) cs_game_node"
trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close> and
\<tau> :: \<open>'a\<close> and
initial :: \<open>('s, 'a) cs_game_node\<close>
begin
subsection \<open>Coupled Simulation Implies Winning Strategy\<close>
fun strategy_from_coupleddsim :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) cs_game_node strategy" where
"strategy_from_coupleddsim R ((DefenderStepNode a p1 q0)#play) =
(AttackerNode p1 (SOME q1 . R p1 q1 \<and> q0 \<longmapsto>^~ a q1))" |
"strategy_from_coupleddsim R ((DefenderCouplingNode p0 q0)#play) =
(AttackerNode (SOME q1 . R q1 p0 \<and> q0 \<longmapsto>* tau q1) p0)" |
"strategy_from_coupleddsim _ _ = undefined"
fun strategy_from_coupleddsim :: \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) cs_game_node strategy\<close> where
\<open>strategy_from_coupleddsim R ((DefenderStepNode a p1 q0)#play) =
(AttackerNode p1 (SOME q1 . R p1 q1 \<and> q0 =\<rhd>a q1))\<close> |
\<open>strategy_from_coupleddsim R ((DefenderCouplingNode p0 q0)#play) =
(AttackerNode (SOME q1 . R q1 p0 \<and> q0 \<longmapsto>* tau q1) p0)\<close> |
\<open>strategy_from_coupleddsim _ _ = undefined\<close>
lemma attacker_followed_by_defender:
lemma defender_preceded_by_attacker:
assumes
"n0 # play \<in> plays"
"cs_game_defender_node n0"
"initial = AttackerNode p0 q0"
shows "\<exists> p q . hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0" "play \<noteq> []"
\<open>n0 # play \<in> plays\<close>
\<open>cs_game_defender_node n0\<close>
\<open>initial = AttackerNode p0 q0\<close>
shows \<open>\<exists> p q . hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> \<open>play \<noteq> []\<close>
proof -
have n0_not_init: "n0 \<noteq> initial" using assms(2,3) by auto
hence "cs_game_moves (hd play) n0" using assms(1)
have n0_not_init: \<open>n0 \<noteq> initial\<close> using assms(2,3) by auto
hence \<open>cs_game_moves (hd play) n0\<close> using assms(1)
by (metis list.sel(1) list.sel(3) plays.cases)
thus "\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0" using assms(2)
by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,7))
show "play \<noteq> []" using n0_not_init assms(1) plays.cases by auto
thus \<open>\<exists>p q. hd play = AttackerNode p q \<and> cs_game_moves (AttackerNode p q) n0\<close> using assms(2)
by (metis cs_game_defender_node.elims(2,3) local.cs_game_moves_no_step(1,2,3,6))
show \<open>play \<noteq> []\<close> using n0_not_init assms(1) plays.cases by auto
qed
lemma defender_only_challenged_by_visible_actions:
assumes
\<open>initial = AttackerNode p0 q0\<close>
\<open>(DefenderStepNode a p q) # play \<in> plays\<close>
shows
\<open>\<not>tau a\<close>
using assms defender_preceded_by_attacker
by fastforce
lemma strategy_from_coupleddsim_retains_coupledsim:
assumes
"R p0 q0"
"coupled_delay_simulation R"
"initial = AttackerNode p0 q0"