...
 
Commits (7)
...@@ -2,7 +2,7 @@ name := "CoupledSim" ...@@ -2,7 +2,7 @@ name := "CoupledSim"
version := "0.1.0" version := "0.1.0"
scalaVersion := "2.11.12" scalaVersion := "2.12.8"
val scalacOpts = Seq( val scalacOpts = Seq(
"-Xmax-classfile-name", "140", "-Xmax-classfile-name", "140",
...@@ -13,7 +13,7 @@ val scalacOpts = Seq( ...@@ -13,7 +13,7 @@ val scalacOpts = Seq(
) )
lazy val web = (project in file("web")).settings( lazy val web = (project in file("web")).settings(
scalaVersion := "2.11.12", scalaVersion := "2.12.8",
scalaJSProjects := Seq(jsClient), scalaJSProjects := Seq(jsClient),
isDevMode in scalaJSPipeline := false, isDevMode in scalaJSPipeline := false,
pipelineStages in Assets := Seq(scalaJSPipeline), pipelineStages in Assets := Seq(scalaJSPipeline),
...@@ -26,7 +26,7 @@ lazy val web = (project in file("web")).settings( ...@@ -26,7 +26,7 @@ lazy val web = (project in file("web")).settings(
).enablePlugins(SbtWeb) ).enablePlugins(SbtWeb)
lazy val shared = (project in file("shared")).settings( lazy val shared = (project in file("shared")).settings(
scalaVersion := "2.11.12", scalaVersion := "2.12.8",
name := "shared", name := "shared",
scalacOptions ++= scalacOpts, scalacOptions ++= scalacOpts,
test in assembly := {}, test in assembly := {},
...@@ -36,7 +36,7 @@ lazy val shared = (project in file("shared")).settings( ...@@ -36,7 +36,7 @@ lazy val shared = (project in file("shared")).settings(
) )
lazy val jsClient = (project in file("js-client")).settings( lazy val jsClient = (project in file("js-client")).settings(
scalaVersion := "2.11.12", scalaVersion := "2.12.8",
name := "coupledsim-client", name := "coupledsim-client",
parallelExecution in ThisBuild := false, parallelExecution in ThisBuild := false,
scalacOptions ++= scalacOpts, scalacOptions ++= scalacOpts,
...@@ -59,20 +59,20 @@ lazy val jsClient = (project in file("js-client")).settings( ...@@ -59,20 +59,20 @@ lazy val jsClient = (project in file("js-client")).settings(
"org.webjars" % "bootstrap" % "3.3.7" / "bootstrap.min.js" "org.webjars" % "bootstrap" % "3.3.7" / "bootstrap.min.js"
), ),
unmanagedSourceDirectories in Compile += 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) ).aggregate(shared).dependsOn(shared).enablePlugins(ScalaJSPlugin, ScalaJSWeb)
val flinkVersion = "1.6.1" val flinkVersion = "1.7.0"
val flinkDependencies = Seq( val flinkDependencies = Seq(
"org.apache.flink" %% "flink-scala" % flinkVersion % "provided", "org.apache.flink" %% "flink-scala" % flinkVersion % "provided",
"org.apache.flink" %% "flink-table" % flinkVersion % "provided", "org.apache.flink" %% "flink-table" % flinkVersion % "provided",
"org.apache.flink" %% "flink-streaming-scala" % 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")). lazy val flink = (project in file("flink")).
settings( settings(
scalaVersion := "2.11.12", scalaVersion := "2.12.8",
resolvers ++= Seq( resolvers ++= Seq(
"Apache Development Snapshot Repository" at "https://repository.apache.org/content/repositories/snapshots/", "Apache Development Snapshot Repository" at "https://repository.apache.org/content/repositories/snapshots/",
Resolver.mavenLocal Resolver.mavenLocal
......
# Coupled Sim Apache Flink program
See [../README.md](../README.md)!
...@@ -390,6 +390,8 @@ object CoupledSimulationFlink { ...@@ -390,6 +390,8 @@ object CoupledSimulationFlink {
CoupledSimulationFlinkBenchmark.runSizeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation) CoupledSimulationFlinkBenchmark.runSizeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation)
} else if (params.has("timemark")) { } else if (params.has("timemark")) {
CoupledSimulationFlinkBenchmark.runTimeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation) CoupledSimulationFlinkBenchmark.runTimeMark(cfgPreminimization = cfgPreminimization, cfgOverApproximation = cfgOverApproximation)
} else if (params.has("tacasmark")) {
TacasBenchmarks.runTacasMark()
} else { } else {
executeAlgorithm(env, executeAlgorithm(env,
cfgPath = cfgPath, cfgPath = cfgPath,
......
...@@ -28,7 +28,7 @@ class SignatureRefinement { ...@@ -28,7 +28,7 @@ class SignatureRefinement {
val oldSigCount: DataSet[Tuple1[Int]] = coloring.map(_._2).distinct.map(_ => Tuple1(1)).sum(0) 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) { 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)] = val signatures: DataSet[(Int, Color)] =
signatureEdges.groupBy(0).reduceGroup { g => 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 package de.bbisping.coupledsim.tool
import scala.scalajs.js.JSApp 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.Action
import de.bbisping.coupledsim.tool.arch.ActionDispatcher import de.bbisping.coupledsim.tool.arch.ActionDispatcher
import de.bbisping.coupledsim.tool.arch.Control import de.bbisping.coupledsim.tool.arch.Control
...@@ -12,7 +12,7 @@ import de.bbisping.coupledsim.tool.view.GraphRenderer ...@@ -12,7 +12,7 @@ import de.bbisping.coupledsim.tool.view.GraphRenderer
import de.bbisping.coupledsim.tool.view.SourceEditor import de.bbisping.coupledsim.tool.view.SourceEditor
import de.bbisping.coupledsim.tool.control.Pipeline import de.bbisping.coupledsim.tool.control.Pipeline
@JSExport @JSExportTopLevel("TransitionSystemFiddle")
object TransitionSystemFiddle extends JSApp with Control with ActionDispatcher { object TransitionSystemFiddle extends JSApp with Control with ActionDispatcher {
val source = new Source(this) val source = new Source(this)
......
...@@ -353,7 +353,7 @@ ...@@ -353,7 +353,7 @@
<script type="text/javascript" src="coupledsim-client-jsdeps.js"></script> <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="js/cm_transitionsystem_mode.js"></script>
<script type="text/javascript" src="coupledsim-client.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> </body>
</html> </html>
...@@ -12,74 +12,74 @@ context lts_tau ...@@ -12,74 +12,74 @@ context lts_tau
begin begin
definition fp_step :: definition fp_step ::
"'s rel \<Rightarrow> 's rel" \<open>'s rel \<Rightarrow> 's rel\<close>
where where
"fp_step R1 \<equiv> { (p,q)\<in>R1. \<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^ a q'))) (\<exists> q'. ((p',q')\<in>R1) \<and> (q \<Rightarrow>^a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }" \<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }\<close>
lemma mono_fp_step: lemma mono_fp_step:
"mono fp_step" \<open>mono fp_step\<close>
proof (rule, safe) proof (rule, safe)
fix x y::"'s rel" and p q fix x y::\<open>'s rel\<close> and p q
assume assume
"x \<subseteq> y" \<open>x \<subseteq> y\<close>
"(p, q) \<in> fp_step x" \<open>(p, q) \<in> fp_step x\<close>
thus "(p, q) \<in> fp_step y" thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def unfolding fp_step_def
by (auto, blast) by (auto, blast)
qed qed
lemma fp_fp_step: lemma fp_fp_step:
assumes assumes
"R = fp_step R" \<open>R = fp_step R\<close>
shows 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 using assms unfolding fp_step_def coupled_simulation_def
by fastforce by fastforce
lemma gfp_fp_step_subset_gcs: 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] unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify proof clarify
fix a b fix a b
assume assume
"(a, b) \<in> gfp fp_step" \<open>(a, b) \<in> gfp fp_step\<close>
thus "a \<sqsubseteq>cs b" thus \<open>a \<sqsubseteq>cs b\<close>
using fp_fp_step mono_fp_step gfp_unfold by auto using fp_fp_step mono_fp_step gfp_unfold by auto
qed qed
lemma fp_fp_step_gcs: lemma fp_fp_step_gcs:
assumes assumes
"R = { (p,q) . greatest_coupled_simulation p q }" \<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows shows
"fp_step R = R" \<open>fp_step R = R\<close>
unfolding assms unfolding assms
proof safe proof safe
fix p q fix p q
assume assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}" \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^ a q')) \<and> 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)" (\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
unfolding fp_step_def by auto 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> 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)" using weak_step_tau2_def by simp (\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close> using weak_step_tau2_def by simp
thus "greatest_coupled_simulation p q" thus \<open>greatest_coupled_simulation p q\<close>
using lts_tau.gcs by metis using lts_tau.gcs by metis
next next
fix p q fix p q
assume assume
"greatest_coupled_simulation p q" \<open>greatest_coupled_simulation p q\<close>
hence "(p, q) \<in> {(x, y). greatest_coupled_simulation x y} \<and> (\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> 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 \<longmapsto>^ a q'))) (\<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))" \<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 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 unfolding fp_step_def by blast
qed 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 using fp_fp_step_gcs gfp_fp_step_subset_gcs
by (simp add: equalityI gfp_upperbound) by (simp add: equalityI gfp_upperbound)
...@@ -89,11 +89,11 @@ context lts_tau_finite ...@@ -89,11 +89,11 @@ context lts_tau_finite
begin begin
lemma gfp_fp_step_while: lemma gfp_fp_step_while:
shows 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 using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast
theorem coupled_sim_fp_step_while: 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 using gfp_fp_step_while gfp_fp_step_gcs by blast
end end
......
section \<open>Fixed Point Algorithm for Coupled Similarity\<close> section \<open>Fixed Point Algorithm for Coupled Similarity\<close>
subsection \<open>The Algorithm\<close>
theory CS_Fixpoint_Algo_Delay theory CS_Fixpoint_Algo_Delay
imports imports
Coupled_Simulation Coupled_Simulation
Finite_Weak_Transition_Systems
"~~/src/HOL/Library/While_Combinator" "~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Finite_Lattice"
begin begin
...@@ -12,83 +14,99 @@ context lts_tau ...@@ -12,83 +14,99 @@ context lts_tau
begin begin
definition fp_step :: definition fp_step ::
"'s rel \<Rightarrow> 's rel" \<open>'s rel \<Rightarrow> 's rel\<close>
where where
"fp_step R1 \<equiv> { (p,q)\<in>R1. \<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^~ a q'))) (tau a \<longrightarrow> (p',q)\<in>R1) \<and>
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }" (\<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: lemma mono_fp_step:
"mono fp_step" \<open>mono fp_step\<close>
proof (rule, safe) proof (rule, safe)
fix x y::"'s rel" and p q fix x y::\<open>'s rel\<close> and p q
assume assume
"x \<subseteq> y" \<open>x \<subseteq> y\<close>
"(p, q) \<in> fp_step x" \<open>(p, q) \<in> fp_step x\<close>
thus "(p, q) \<in> fp_step y" thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def unfolding fp_step_def
by (auto, blast) by (auto, blast)
qed qed
thm prod.simps(2)
lemma fp_fp_step: lemma fp_fp_step:
assumes assumes
"R = fp_step R" \<open>R = fp_step R\<close>
shows 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 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: 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] unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify proof clarify
fix a b fix a b
assume assume
"(a, b) \<in> gfp fp_step" \<open>(a, b) \<in> gfp fp_step\<close>
thus "a \<sqsubseteq>cs b" thus \<open>a \<sqsubseteq>cs b\<close>
unfolding coupled_sim_by_eq_delay_coupled_simulation unfolding coupled_sim_by_eq_coupled_delay_simulation
using fp_fp_step mono_fp_step gfp_unfold using fp_fp_step mono_fp_step gfp_unfold
by metis by metis
qed qed
lemma fp_fp_step_gcs: lemma fp_fp_step_gcs:
assumes assumes
"R = { (p,q) . greatest_coupled_simulation p q }" \<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows shows
"fp_step R = R" \<open>fp_step R = R\<close>
unfolding assms unfolding assms
proof safe proof safe
fix p q fix p q
assume assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}" \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^~ a q')) \<and> hence
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)" \<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 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> 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)" (\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
unfolding fp_step_def using weak_step_delay_implies_weak_tau by blast unfolding fp_step_def using weak_step_delay_implies_weak_tau steps.refl by blast
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^^ a q')) \<and> 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)" using weak_step_tau2_def by simp (\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)\<close>
thus "greatest_coupled_simulation p q" using weak_step_tau2_def by simp
thus \<open>greatest_coupled_simulation p q\<close>
using lts_tau.gcs by metis using lts_tau.gcs by metis
next next
fix p q fix p q
assume asm: assume asm:
"greatest_coupled_simulation p q" \<open>greatest_coupled_simulation p q\<close>
then have "(p, q) \<in> {(x, y). greatest_coupled_simulation x y}" by blast 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> 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 . unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_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')))" moreover from asm have \<open>\<forall> p' a. p \<longmapsto>a p' \<and> \<not>tau a \<longrightarrow>
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_delay_coupled_simulation (\<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) 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 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 unfolding fp_step_def by blast
qed 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 using fp_fp_step_gcs gfp_fp_step_subset_gcs
by (simp add: equalityI gfp_upperbound) by (simp add: equalityI gfp_upperbound)
...@@ -98,14 +116,14 @@ context lts_tau_finite ...@@ -98,14 +116,14 @@ context lts_tau_finite
begin begin
lemma gfp_fp_step_while: lemma gfp_fp_step_while:
shows 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 using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast
theorem coupled_sim_fp_step_while: 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 using gfp_fp_step_while gfp_fp_step_gcs by blast
end end
end end
This source diff could not be displayed because it is too large. You can view the blob instead.
section \<open>Preliminaries\<close>
subsection \<open>Some Utilities for Finite Partial Orders\<close>
text \<open>For some reason there seems to be no Isaeblle support for maximal elements in finite regions
of incomplete partial orders (such as the transitive step relation in cycle-compressed transition
systems ;).)\<close>
theory Finite_Partial_Order
imports Main
begin
context preorder
begin
lemma foldl_max_inflation:
\<open>foldl max x0 xs \<le> foldl max x0 (xs @ [x])\<close>
unfolding foldl_append foldl.simps
by (simp add: ord.max_def)
lemma foldl_max_soundness:
shows
\<open>foldl max x0 (x0 # xs) \<in> set (x0 # xs)\<close>
proof (induct xs rule: rev_induct)
case Nil
then show ?case by (auto simp add: max_def)
next
case (snoc x xs)
then show ?case unfolding foldl_append max_def by auto
qed
lemma foldl_max_maximal:
shows
\<open>\<forall> y \<in> set (x0 # xs). foldl max x0 (x0 # xs) \<le> y \<longrightarrow> y \<le> foldl max x0 (x0 # xs)\<close>
proof (induct xs rule: rev_induct)
case Nil
then show ?case by (auto simp add: max_def)
next
case (snoc x xs)
then show ?case unfolding foldl.simps foldl_append
by (metis Un_insert_right append_Nil2 foldl_Cons insert_iff list.simps(15) local.order_refl
local.order_trans ord.max_def set_append snoc.hyps)
qed
end
context order \<comment>\<open>that is: partial order\<close>
begin
lemma finite_max:
fixes q
defines \<open>above_q \<equiv> {q'. q \<le> q'}\<close>
assumes
\<open>finite above_q\<close>
shows
\<open>\<exists> q_max. q_max \<in> above_q \<and> (\<forall> q''\<in> above_q. q_max \<le> q'' \<longrightarrow> q'' = q_max)\<close>
proof -
have \<open>q \<in> above_q\<close> unfolding above_q_def by blast
then obtain above_list where above_list_spec: \<open>set (q#above_list) = above_q\<close>
using \<open>finite above_q\<close> finite_list by auto
define q_max where \<open>q_max \<equiv> foldl max q (q#above_list)\<close>
have \<open>q_max \<in> above_q\<close>
unfolding q_max_def above_list_spec[symmetric] using foldl_max_soundness .
moreover have \<open>\<forall> q'' \<in> above_q. q_max \<le> q'' \<longrightarrow> q'' = q_max\<close>
unfolding q_max_def above_list_spec[symmetric] using foldl_max_maximal antisym by blast
ultimately show ?thesis by blast
qed
end
end
\ No newline at end of file
...@@ -3,11 +3,10 @@ session "Coupled_Simulation" = "HOL" + ...@@ -3,11 +3,10 @@ session "Coupled_Simulation" = "HOL" +
theories [quick_and_dirty, document = false] theories [quick_and_dirty, document = false]
"~~/src/HOL/Library/While_Combinator" "~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Finite_Lattice"
theories [quick_and_dirty] theories
CS_Fixpoint_Algo
CS_Game
CS_Fixpoint_Algo_Delay CS_Fixpoint_Algo_Delay
CS_Game_Delay CS_Game_Delay
document_files document_files
"root.tex" "root.tex"
(*"root.bib"*) "root.bib"
"splncs04.bst"
...@@ -8,53 +8,65 @@ begin ...@@ -8,53 +8,65 @@ begin
text \<open>Simple games are games where player0 wins all infinite plays.\<close> text \<open>Simple games are games where player0 wins all infinite plays.\<close>
locale simple_game = locale simple_game =
fixes fixes
game_move :: "'s \<Rightarrow> 's \<Rightarrow> bool" ("_ \<longmapsto>\<heartsuit> _" [70, 70] 80) and game_move :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<longmapsto>\<heartsuit> _" [70, 70] 80) and
player0_position :: "'s \<Rightarrow> bool" and player0_position :: \<open>'s \<Rightarrow> bool\<close> and
initial :: 's initial :: 's
begin begin
definition player1_position :: "'s \<Rightarrow> bool" definition player1_position :: \<open>'s \<Rightarrow> bool\<close>
where "player1_position s \<equiv> \<not> player0_position s" where \<open>player1_position s \<equiv> \<not> player0_position s\<close>
\<comment>\<open>plays (to be precise: play p refixes) are lists. we model them \<comment>\<open>plays (to be precise: play p refixes) are lists. we model them
with the most recent move at the beginning. (for our purpose it's enough to consider finite plays)\<close> with the most recent move at the beginning. (for our purpose it's enough to consider finite plays)\<close>
type_synonym ('s2) play = "'s2 list" type_synonym ('s2) play = \<open>'s2 list\<close>
type_synonym ('s2) strategy = "'s2 play \<Rightarrow> 's2" type_synonym ('s2) strategy = \<open>'s2 play \<Rightarrow> 's2\<close>
inductive_set plays :: "'s play set" where inductive_set plays :: \<open>'s play set\<close> where
"[initial] \<in> plays" | \<open>[initial] \<in> plays\<close> |
"p#play \<in> plays \<Longrightarrow> p \<longmapsto>\<heartsuit> p' \<Longrightarrow> p'#p#play \<in> plays" \<open>p#play \<in> plays \<Longrightarrow> p \<longmapsto>\<heartsuit> p' \<Longrightarrow> p'#p#play \<in> plays\<close>
\<comment>\<open>plays for a given player 0 strategy\<close> \<comment>\<open>plays for a given player 0 strategy\<close>
inductive_set plays_for_strategy :: "'s strategy \<Rightarrow> 's play set" for f where inductive_set plays_for_strategy :: \<open>'s strategy \<Rightarrow> 's play set\<close> for f where
init: "[initial] \<in> plays_for_strategy f" | init: \<open>[initial] \<in> plays_for_strategy f\<close> |
p0move: "n0#play \<in> plays_for_strategy f \<Longrightarrow> player0_position n0 \<Longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play) p0move: \<open>n0#play \<in> plays_for_strategy f \<Longrightarrow> player0_position n0 \<Longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)
\<Longrightarrow> (f (n0#play))#n0#play \<in> plays_for_strategy f" | \<Longrightarrow> (f (n0#play))#n0#play \<in> plays_for_strategy f\<close> |
p1move: "n1#play \<in> plays_for_strategy f \<Longrightarrow> player1_position n1 \<Longrightarrow> n1 \<longmapsto>\<heartsuit> n1' p1move: \<open>n1#play \<in> plays_for_strategy f \<Longrightarrow> player1_position n1 \<Longrightarrow> n1 \<longmapsto>\<heartsuit> n1'
\<Longrightarrow> n1'#n1#play \<in> plays_for_strategy f" \<Longrightarrow> n1'#n1#play \<in> plays_for_strategy f\<close>
lemma strategy_step:
assumes
\<open>n0 # n1 # rest \<in> plays_for_strategy f\<close>
\<open>player0_position n1\<close>
shows
\<open>f (n1 # rest) = n0\<close>
using assms
by (induct rule: plays_for_strategy.cases, auto simp add: simple_game.player1_position_def)
definition positional_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
\<open>positional_strategy f \<equiv> \<forall>r1 r2 n. f (n # r1) = f (n # r2)\<close>
text \<open>a strategy is sound if it only decides on enabled transitions.\<close> text \<open>a strategy is sound if it only decides on enabled transitions.\<close>
definition sound_strategy :: "'s strategy \<Rightarrow> bool" where definition sound_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
"sound_strategy f \<equiv> \<open>sound_strategy f \<equiv>
\<forall> n0 play . n0#play \<in> plays_for_strategy f \<and> player0_position n0 \<longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)" \<forall> n0 play . n0#play \<in> plays_for_strategy f \<and> player0_position n0 \<longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)\<close>
lemma strategy_plays_subset: lemma strategy_plays_subset:
assumes "play \<in> plays_for_strategy f" assumes \<open>play \<in> plays_for_strategy f\<close>
shows "play \<in> plays" shows \<open>play \<in> plays\<close>
using assms by (induct rule: plays_for_strategy.induct, auto simp add: plays.intros) using assms by (induct rule: plays_for_strategy.induct, auto simp add: plays.intros)
lemma no_empty_plays: lemma no_empty_plays:
assumes "[] \<in> plays" assumes \<open>[] \<in> plays\<close>
shows "False" shows \<open>False\<close>
using assms plays.cases by blast using assms plays.cases by blast
text \<open>player1 wins a play if the play has reached a deadlock where it's player0's turn\<close>
text"player1 wins a play if the play has reached a deadlock where it's player0's turn" definition player1_wins :: \<open>'s play \<Rightarrow> bool\<close> where
definition player1_wins :: "'s play \<Rightarrow> bool" where \<open>player1_wins play \<equiv> player0_position (hd play) \<and> (\<nexists> p' . (hd play) \<longmapsto>\<heartsuit> p')\<close>
"player1_wins play \<equiv> player0_position (hd play) \<and> (\<nexists> p' . (hd play) \<longmapsto>\<heartsuit> p')"
definition player0_winning_strategy :: "'s strategy \<Rightarrow> bool" where definition player0_winning_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
"player0_winning_strategy f \<equiv> (\<forall> play \<in> plays_for_strategy f . \<not> player1_wins play)" \<open>player0_winning_strategy f \<equiv> (\<forall> play \<in> plays_for_strategy f . \<not> player1_wins play)\<close>
end end
......
section \<open>Strong Simulation and Bisimulation\<close> section \<open>Notions of Equivalence\<close>
subsection \<open>Strong Simulation and Bisimulation\<close>
theory Strong_Relations theory Strong_Relations
imports Transition_Systems imports Transition_Systems
...@@ -8,37 +10,29 @@ context lts ...@@ -8,37 +10,29 @@ context lts
begin begin
definition simulation :: definition simulation ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
"simulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto> a q')))"
definition simulation_on ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's set \<Rightarrow> 's set \<Rightarrow> bool"
where where
"simulation_on R S1 S2 \<equiv> \<forall> p \<in> S1. \<forall> q \<in> S2. R p q \<longrightarrow> \<open>simulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' \<in> S1 . \<forall> a . p \<longmapsto> a p' \<longrightarrow> (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q' \<in> S2 . R p' q' \<and> (q \<longmapsto> a q')))" (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q')))\<close>
definition bisimulation :: definition bisimulation ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where where
"bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow> \<open>bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto> a q'))) \<and> (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))) \<and>
(\<forall> q' a. q \<longmapsto> a q' \<longrightarrow> (\<forall> q' a. q \<longmapsto>a q' \<longrightarrow>
(\<exists> p'. R p' q' \<and> (p \<longmapsto> a p')))" (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p')))\<close>
lemma bisim_ruleformat: lemma bisim_ruleformat:
assumes "bisimulation R" assumes \<open>bisimulation R\<close>
and "R p q" and \<open>R p q\<close>
shows shows
"p \<longmapsto> a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto> a q'))" \<open>p \<longmapsto>a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))\<close>
"q \<longmapsto> a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto> a p'))" \<open>q \<longmapsto>a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p'))\<close>
using assms unfolding bisimulation_def by auto using assms unfolding bisimulation_def by auto
end \<comment>\<open>context lts\<close> end \<comment>\<open>context lts\<close>
end end
section \<open>Transition Systems\<close> subsection \<open>Labeled Transition Systems\<close>
theory Transition_Systems theory Transition_Systems
imports Main imports Finite_Partial_Order
begin begin
locale lts = locale lts =
fixes fixes
trans :: "'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>
begin begin
abbreviation step_pred :: "'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool" where abbreviation step_pred :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
"step_pred p af q \<equiv> \<exists> a. af a \<and> trans p a q" where
\<open>step_pred p af q \<equiv> \<exists> a. af a \<and> trans p a q\<close>
abbreviation step :: abbreviation step ::
"'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>
("_ \<longmapsto>_ _" [70, 70, 70] 80) ("_ \<longmapsto>_ _" [70, 70, 70] 80)
where where
"p \<longmapsto>a q \<equiv> trans p a q" \<open>p \<longmapsto>a q \<equiv> trans p a q\<close>
inductive steps :: "'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool" inductive steps :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
("_ \<longmapsto>* _ _" [70, 70, 70] 80) ("_ \<longmapsto>* _ _" [70, 70, 70] 80)
where where
refl: "p \<longmapsto>* af p" refl: \<open>p \<longmapsto>* A p\<close> | step: \<open>p \<longmapsto>* A q1 \<Longrightarrow> q1 \<longmapsto>a q \<Longrightarrow> A a \<Longrightarrow> (p \<longmapsto>* A q)\<close>
| step: "p \<longmapsto>* af q1 \<Longrightarrow> q1 \<longmapsto> a q \<Longrightarrow> af a \<Longrightarrow> (p \<longmapsto>* af q)"
lemma steps_one_step: lemma steps_one_step:
assumes assumes
"p \<longmapsto> a p'" \<open>p \<longmapsto>a p'\<close>
"A a" \<open>A a\<close>
shows shows
"p \<longmapsto>* A p'" \<open>p \<longmapsto>* A p'\<close> using steps.step[of p A p a p'] steps.refl[of p A] assms .
using steps.step[of p A p a p'] steps.refl[of p A] assms .
lemma steps_concat:
assumes
\<open>p' \<longmapsto>* A p''\<close>
\<open>p \<longmapsto>* A p'\<close>
shows
\<open>p \<longmapsto>* A p''\<close> using assms
proof (induct arbitrary: p)
case (refl p'' A p')
then show ?case by auto
next
case (step p' A p'' a pp p)
hence \<open>p \<longmapsto>* A p''\<close> by simp
show ?case using steps.step[OF `p \<longmapsto>* A p''` step(3,4)] .
qed
lemma steps_left: lemma steps_left:
assumes assumes
"p \<noteq> p'" \<open>p \<noteq> p'\<close>
"p \<longmapsto>* A p'" \<open>p \<longmapsto>* A p'\<close>
shows shows
"\<exists>p'' a . p \<longmapsto> a p'' \<and> A a" \<open>\<exists>p'' a . p \<longmapsto>a p'' \<and> A a \<and> p'' \<longmapsto>* A p'\<close>
using assms(2,1) by (induct, auto) using assms(1)
by (induct rule:steps.induct[OF assms(2)], blast, metis refl steps_concat steps_one_step)
lemma steps_no_step: lemma steps_no_step:
assumes assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> \<not>A a" \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
"p \<noteq> p''" \<open>p \<noteq> p''\<close>
"p \<longmapsto>* A p''" \<open>p \<longmapsto>* A p''\<close>
shows shows
"False" \<open>False\<close>
using steps_left[OF assms(2,3)] assms(1) by blast using steps_left[OF assms(2,3)] assms(1) by blast
lemma steps_no_step_pos: lemma steps_no_step_pos:
assumes assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> \<not>A a" \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
"p \<longmapsto>* A p'" \<open>p \<longmapsto>* A p'\<close>
shows shows
"p = p'" \<open>p = p'\<close>
using assms steps_no_step by blast using assms steps_no_step by blast
lemma steps_loop: lemma steps_loop:
assumes assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> p = p'" \<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> p = p'\<close>
"p \<noteq> p''" \<open>p \<noteq> p''\<close>
"p \<longmapsto>* A p''" \<open>p \<longmapsto>* A p''\<close>
shows shows
"False" \<open>False\<close>
using assms(3,1,2) by (induct, auto) using assms(3,1,2) by (induct, auto)
lemma steps_concat:
assumes corollary steps_transp:
"p' \<longmapsto>* A p''" \<open>transp (\<lambda> p p'. p \<longmapsto>* A p')\<close>
"p \<longmapsto>* A p'" using steps_concat unfolding transp_def by blast
shows
"p \<longmapsto>* A p''"
using assms proof (induct arbitrary: p)
case (refl p'' A p')
then show ?case by auto
next
case (step p' A p'' a pp p)
hence "p \<longmapsto>* A p''" by simp
show ?case using steps.step[OF `p \<longmapsto>* A p''` step(3,4)] .
qed
lemma steps_spec: lemma steps_spec:
assumes assumes
"p \<longmapsto>* A' p'" \<open>p \<longmapsto>* A' p'\<close>
"\<And> a . A' a \<Longrightarrow> A a" \<open>\<And> a . A' a \<Longrightarrow> A a\<close>
shows shows
"p \<longmapsto>* A p'" \<open>p \<longmapsto>* A p'\<close> using assms(1,2)
using assms(1,2) proof induct proof induct
case (refl p) case (refl p)
show ?case using steps.refl . show ?case using steps.refl .
next next
case (step p A' pp a pp') case (step p A' pp a pp')
hence "p \<longmapsto>* A pp" by simp hence \<open>p \<longmapsto>* A pp\<close> by simp
then show ?case using step(3,4,5) steps.step by auto then show ?case using step(3,4,5) steps.step by auto
qed qed
text\<open>If one can reach only a finite portion of the graph following @{text "\<longmapsto>* A"}, interpretation preorder \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
by (standard, simp, simp add: steps.refl, metis steps_concat)
text\<open>If one can reach only a finite portion of the graph following @{text \<open>\<longmapsto>* A\<close>},
and all cycles are loops, then there must be nodes which are maximal wrt. \<open>\<longmapsto>* A\<close>.\<close> and all cycles are loops, then there must be nodes which are maximal wrt. \<open>\<longmapsto>* A\<close>.\<close>
lemma step_max_deadlock: lemma step_max_deadlock:
fixes A q fixes A q
assumes assumes
"\<And> r1 r2. r1 \<longmapsto>* A r2 \<and> r2 \<longmapsto>* A r1 \<Longrightarrow> r1 = r2" \<comment>\<open>contracted cycles (anti-symmetry)\<close> antiysmm: \<open>\<And> r1 r2. r1 \<longmapsto>* A r2 \<and> r2 \<longmapsto>* A r1 \<Longrightarrow> r1 = r2\<close> and
"finite {q'. q \<longmapsto>* A q'}" finite: \<open>finite {q'. q \<longmapsto>* A q'}\<close> and
"\<forall> q'. q \<longmapsto>* A q' \<longrightarrow> (\<exists>q''. q' \<longmapsto>* A q'' \<and> q' \<noteq> q'')" no_max: \<open>\<forall> q'. q \<longmapsto>* A q' \<longrightarrow> (\<exists>q''. q' \<longmapsto>* A q'' \<and> q' \<noteq> q'')\<close>
shows shows
False False
using assms proof -
sorry \<comment>\<open>this should be easy to prove if i understood anything about \<open>finite\<close> in isabelle..\<close> interpret order \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
by (standard, simp add: assms(1))
show ?thesis using local.finite_max assms local.order_trans mem_Collect_eq by metis
qed
end \<comment>\<open>end of lts\<close> end \<comment>\<open>end of lts\<close>
lemma lts_impl_steps2: lemma lts_impl_steps2:
assumes assumes
"lts.steps step1 p1 ap p2" \<open>lts.steps step1 p1 ap p2\<close>
"\<And> p1 a p2 . step1 p1 a p2 \<and> P p1 a p2 \<Longrightarrow> step2 p1 a p2" \<open>\<And> p1 a p2 . step1 p1 a p2 \<and> P p1 a p2 \<Longrightarrow> step2 p1 a p2\<close>
"\<And> p1 a p2 . P p1 a p2" \<open>\<And> p1 a p2 . P p1 a p2\<close>
shows shows
"lts.steps step2 p1 ap p2" \<open>lts.steps step2 p1 ap p2\<close>
proof (induct rule: lts.steps.induct[OF assms(1)]) proof (induct rule: lts.steps.induct[OF assms(1)])
case (1 p af) case (1 p af)
show ?case using lts.steps.refl[of step2 p af] by blast show ?case using lts.steps.refl[of step2 p af] by blast
next next
case (2 p af q1 a q) case (2 p af q1 a q)
hence "step2 q1 a q" using assms(2,3) by blast hence \<open>step2 q1 a q\<close> using assms(2,3) by blast
thus ?case using lts.step[OF 2(2) _ 2(4)] by blast thus ?case using lts.step[OF 2(2) _ 2(4)] by blast
qed qed
lemma lts_impl_steps: lemma lts_impl_steps:
assumes assumes
"lts.steps step1 p1 ap p2" \<open>lts.steps step1 p1 ap p2\<close>
"\<And> p1 a p2 . step1 p1 a p2 \<Longrightarrow> step2 p1 a p2" \<open>\<And> p1 a p2 . step1 p1 a p2 \<Longrightarrow> step2 p1 a p2\<close>
shows shows
"lts.steps step2 p1 ap p2" \<open>lts.steps step2 p1 ap p2\<close>
using assms lts_impl_steps2[OF assms] by auto using assms lts_impl_steps2[OF assms] by auto
end end
\ No newline at end of file