diff --git a/examples/scholarly_paper/2022-RAS-SI/ROOT b/examples/scholarly_paper/2022-RAS-SI/ROOT index eff13c4..1386a45 100644 --- a/examples/scholarly_paper/2022-RAS-SI/ROOT +++ b/examples/scholarly_paper/2022-RAS-SI/ROOT @@ -7,3 +7,13 @@ session "2022-RAS-SI" = "Isabelle_DOF" + "root.bib" "preamble.tex" "build" + "figures/AcVecSpaceVsSpeedVs.png" + "figures/actor_def.png" + "figures/MaxwellVsCutIn.png" + "figures/actor_driving_strategy_inclusion.png" + "figures/RSS_Safe_Longitudinal_Distance.png" + "figures/actor_driving_strategy_ref.png" + "figures/RSS_formula.png" + "figures/demon_def.png" + "figures/Samplings.png" + "figures/scenarios_def.png" diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/AcVecSpaceVsSpeedVs.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/AcVecSpaceVsSpeedVs.png new file mode 100644 index 0000000..bccf5d3 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/AcVecSpaceVsSpeedVs.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/MaxwellVsCutIn.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/MaxwellVsCutIn.png new file mode 100644 index 0000000..4de728b Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/MaxwellVsCutIn.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_Safe_Longitudinal_Distance.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_Safe_Longitudinal_Distance.png new file mode 100644 index 0000000..7a9881d Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_Safe_Longitudinal_Distance.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_formula.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_formula.png new file mode 100644 index 0000000..d97c9ab Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/RSS_formula.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/Samplings.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/Samplings.png new file mode 100644 index 0000000..032e0f1 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/Samplings.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_def.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_def.png new file mode 100644 index 0000000..9cb4635 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_def.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_inclusion.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_inclusion.png new file mode 100644 index 0000000..0dbc970 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_inclusion.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_ref.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_ref.png new file mode 100644 index 0000000..d29d36b Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/actor_driving_strategy_ref.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/demon_def.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/demon_def.png new file mode 100644 index 0000000..5461f09 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/demon_def.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/document/figures/scenarios_def.png b/examples/scholarly_paper/2022-RAS-SI/document/figures/scenarios_def.png new file mode 100644 index 0000000..69d8eb4 Binary files /dev/null and b/examples/scholarly_paper/2022-RAS-SI/document/figures/scenarios_def.png differ diff --git a/examples/scholarly_paper/2022-RAS-SI/paper.thy b/examples/scholarly_paper/2022-RAS-SI/paper.thy index dc6c872..288df21 100644 --- a/examples/scholarly_paper/2022-RAS-SI/paper.thy +++ b/examples/scholarly_paper/2022-RAS-SI/paper.thy @@ -178,13 +178,14 @@ text\At a glance, the overall concepts and notions we are using here are l \ \S\x\B. P x
, |||x\B. P x, ||x\B. P x, SEQ x\B. P x\ (for infinite index sets A, finite sets B) \<^item> A typed view on processes with Hindley-Milner Polymorphism; - (operators and process-schemata are typed over \'\ process\) + (operators and are typed over \'\ process\; + process-schemata are just higher-order functions over processes.) \<^item> Denotationally defined notions for traces \\\, failures \\\, and divergences \\\ \<^item> Proof Theory for refinement notions on processes: \\\<^sub>\, \\<^sub>\, \\<^sub>\\<^sub>\\ \ \\too long the rest\ - +(* text\ Generalizations of these two operators \\x\A. P(x)\ and \\x\A. P(x)\ allow for modeling the concepts of \<^emph>\input\ and \<^emph>\output\: Based on the prefix operator \a\P\ (event \a\ happens, then the process @@ -209,7 +210,11 @@ with dynamic thread creation, and processes with unbounded thread-local variable However, this adds substantial complexity to the process theory: when it comes to study the interplay of different denotational models, refinement-orderings, and side-conditions for continuity, paper-and-pencil proofs easily reach their limits of precision. +*) +subsection\Isabelle and HOL-CSP\ +\ \too long and partially off-topic\ +text\ Several attempts have been undertaken to develop a formal theory in an interactive proof system, mostly in Isabelle/HOL @{cite "Camilleri91" and "tej.ea:corrected:1997" and "IsobeRoggenbach2010" and "DBLP:journals/afp/Noce16"}. @@ -231,6 +236,38 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc \<^url>\https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0\. In this paper, all Isabelle proofs are omitted.\}. \ + +subsection\RSS\ +text\ +Two Cars, “current” set of 
assumptions Safety Property: +\<^item> reaction time ( \>> \t\): \\\ +\<^item> minimal distance to be respected : \d\<^sub>m\<^sub>i\<^sub>n\ +\<^item> speeds for “rear” and “front” cars: \v\<^sub>r\,\v\<^sub>f\ +\ + + +figure*[AcVecSpaceVsSpeedVs::figure,relative_width="100",src="''figures/AcVecSpaceVsSpeedVs.png''"] + \Acceleration Vector Space vs. Speed Vectors \ +figure*[MaxwellVsCutIn::figure,relative_width="100",src="''figures/MaxwellVsCutIn.png''"] + \Maxwell's Daemon vs. Cut-In Scenarios\ +figure*[RSS_Safe_Longitudinal_Distance::figure,relative_width="100",src="''figures/RSS_Safe_Longitudinal_Distance.png''"] + \Safe Longitudinal Distance in RSS\ +figure*[RSS_formula::figure,relative_width="100",src="''figures/RSS_formula.png''"] + \The Formula of RSS\ +figure*[Samplings::figure,relative_width="100",src="''figures/Samplings.png''"] + \Samplings of Continuous Observables\ +figure*[actor_def::figure,relative_width="100",src="''figures/actor_def.png''"] + \Definition of Actors\ +figure*[demon_def::figure,relative_width="100",src="''figures/demon_def.png''"] + \Definition of a Maxwell-Demon\ +figure*[scenarios_def::figure,relative_width="100",src="''figures/scenarios_def.png''"] + \Definition of Scenarios\ +figure*[actor_driving_strategy_inclusion::figure,relative_width="100",src="''figures/actor_driving_strategy_inclusion.png''"] + \Trace Inclusion of Actors Parameterized by Driving Strategies\ +figure*[actor_driving_strategy_ref::figure,relative_width="100",src="''figures/actor_driving_strategy_ref.png''"] + \Refining Actors Parameterized by Driving Strategies\ + + (* % Moreover, decomposition rules of the form: % \begin{center} @@ -244,8 +281,10 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc % way for future tool combinations for model-checkers such as FDR4~@{cite "fdr4"} or % PAT~@{cite "SunLDP09"} based on proof certifications.*) -section*["pre"::tc,main_author="Some(@{docitem \bu\}::author)"] - \Appendix\ +subsection\\ + + +section*["pre"::tc,main_author="Some(@{docitem \bu\}::author)"] \Appendix\ text\Just Examples in Copy-Paste and best-practices in Isabelle/DOF\