Merge remote-tracking branch 'origin/pre_merge_robochart'

ITree_Deadlock.thy

@@ -9,6 +9,8 @@ text \<open> Deadlock is an interaction with no visible event \<close>
 definition deadlock :: "('e, 'r) itree" where
 "deadlock = Vis {}\<^sub>p"
 
+abbreviation stop where "stop \<equiv> deadlock"
+
 lemma stable_deadlock [simp]: "stable deadlock"
   by (simp add: deadlock_def)
 

ROOT

@@ -30,6 +30,7 @@ session "ITree_RoboChart" in "RoboChart" = "ITree_UTP" +
   options [timeout = 600, document = pdf, document_output = "output"]
   theories
     ITree_RoboChart
+    RoboChart_Simulation
   document_files
     "root.tex"
 
@@ -49,6 +50,7 @@ session "RoboChart_ChemicalDetector_autonomous" in "RoboChart/examples/RoboChart
   options [timeout = 600, document = pdf, document_output = "output"]
   sessions
     "ITree_RoboChart"
+    "ITree_Simulation"
   theories
     RoboChart_ChemicalDetector_autonomous 
   document_files

RoboChart/ITree_RoboChart.thy

@@ -1,26 +1,69 @@
 section \<open> RoboChart semantics \<close>
 
 theory ITree_RoboChart
-  imports "Interaction_Trees.ITree_Extraction" "HOL-Library.Numeral_Type" 
+  imports "Interaction_Trees.ITree_Extraction"
+          "Interaction_Trees.ITree_Deadlock"
+          "HOL-Library.Numeral_Type" 
           "ITree_UTP.ITree_CSP_Biased"
 begin
 
 unbundle Z_Relation_Syntax
 
 subsection \<open> CSP operators \<close>
-definition stop where "stop = deadlock"
 
 definition par_hide where
 "par_hide P s Q = (hide (P \<parallel>\<^bsub> s \<^esub> Q) s)"
 
 text \<open> Events are hidden based on their order in a list. \<close>
-definition prhide where
-"prhide P es = foldl (\<lambda> Q e. hide Q {e}) P es"
+definition hidep (infixl "\<setminus>\<^sub>p" 90) where 
+"hidep P es = foldl (\<lambda> Q e. hide Q {e}) P es"
+
+definition par_hidep where
+"par_hidep P s Q = (hidep (P \<parallel>\<^bsub> set s \<^esub> Q) s)"
 
 text \<open> A process's state must be discarded before being in parallel composition. \<close>
 definition discard_state where
 "discard_state P = do {P ; skip}"
 
+term "map_pfun"
+term "rename a"
+
+text \<open> Domain restriction of an associative list \<close>
+definition rel_domres_l :: "'a set \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" (infixr "\<lhd>\<^sub>r\<^sub>l" 85) where
+"rel_domres_l A al = [m. m \<leftarrow> al, fst m \<in> A]"
+
+text \<open> Drop pairs @{text "(x,y)"} where @{text "y"} is in @{text "A"}. 
+
+With this definition, we can give priority to the pair with a small index and remove remaining pairs 
+with the same value in the image. 
+
+For example, @{text "filter_out [(a1, b1), (a2, b2), (a3, b1)] = [(a1, b1), (a2, b2)]"}
+where @{text "(a3, b1)"} is filtered out because @{text "b1"} is mapped to @{text "a1"} in the 
+beginning of the list.
+\<close>
+primrec drop_dup :: "('a \<times> 'b) list \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) list" where 
+"drop_dup [] A = []" |
+"drop_dup (x#xs) A = 
+  (if (snd x) \<in> A then (drop_dup xs A) 
+ else (x # (drop_dup xs (A \<union> {snd x}))))"
+
+value "drop_dup [(1, 2), (2, 3), (3, 2)] {}::(int \<times> int) list"
+
+abbreviation "drop_dup' l \<equiv> drop_dup l {}"
+
+text \<open> Another form of renaming whose renaming maps are an associative list. Priority, therefore, 
+can be given to the pairs in the beginning of the list when renaming causes nondeterminism. 
+\<close>
+primcorec renamep :: "('e\<^sub>1 \<times> 'e\<^sub>2) list \<Rightarrow> ('e\<^sub>1, 'a) itree \<Rightarrow> ('e\<^sub>2, 'a) itree" where
+"renamep \<rho> P = 
+  (case P of
+    Ret x \<Rightarrow> Ret x |
+    Sil P \<Rightarrow> Sil (renamep \<rho> P) |
+    Vis F \<Rightarrow> Vis (map_pfun (renamep \<rho>) (F \<circ>\<^sub>p graph_pfun ((set (drop_dup' (pdom F \<lhd>\<^sub>r\<^sub>l \<rho>)))\<inverse>))))"
+
+abbreviation renamep':: "('e\<^sub>1, 'a) itree \<Rightarrow> ('e\<^sub>1 \<times> 'e\<^sub>2) list \<Rightarrow> ('e\<^sub>2, 'a) itree" ("_\<lbrace>_\<rbrace>\<^sub>p" 59) where
+"renamep' P \<rho> \<equiv> renamep \<rho> P"
+
 subsection \<open> RoboChart types \<close>
 type_synonym core_bool = bool
 type_synonym core_nat = natural
@@ -122,6 +165,34 @@ datatype InOut = din | dout
 definition "InOut_list = [din, dout]"
 definition "InOut_set = set InOut_list"
 
+instantiation InOut :: enum
+begin
+definition enum_InOut :: "InOut list" where
+"enum_InOut = InOut_list"
+
+definition enum_all_InOut :: "(InOut \<Rightarrow> bool) \<Rightarrow> bool" where
+"enum_all_InOut P = (\<forall>b :: InOut \<in> set enum_class.enum. P b)"
+
+definition enum_ex_InOut :: "(InOut \<Rightarrow> bool) \<Rightarrow> bool" where
+"enum_ex_InOut P = (\<exists>b ::  InOut \<in> set enum_class.enum. P b)"
+
+instance
+proof (intro_classes)
+  show "distinct (enum_class.enum :: InOut list)"
+    by (simp add: enum_InOut_def InOut_list_def)
+
+  show univ_eq: "UNIV = set (enum_class.enum:: InOut list)"
+    apply (simp add: enum_InOut_def InOut_list_def)
+    apply (auto simp add: enum_UNIV)
+    by (meson InOut.exhaust)
+
+  fix P :: "InOut \<Rightarrow> bool"
+  show "enum_class.enum_all P = Ball UNIV P"
+    and "enum_class.enum_ex P = Bex UNIV P" 
+    by (simp_all add: univ_eq enum_all_InOut_def enum_ex_InOut_def)
+qed
+end
+
 subsection \<open> Channels and Events\<close>
 text \<open> The @{text "mapfc"} and @{text "mapf"} together are used to enumerate events 
 for a collection of channels. \<close>

RoboChart/README.md

@@ -1,29 +1,17 @@
 This folder contains theories and examples for animation of RoboChart.
 
-# Installation
-1. Download and install [Isabelle2021](https://isabelle.in.tum.de/index.html).
-2. Install GHC for Haskell, see [here](https://www.haskell.org/platform/) for details.
-2. Clone the following repositories inside a folder (for example, `/path/to/repos`).
-- [Mirror AFP 2021](https://github.com/isabelle-utp/mirror-afp-2021)
-- [Z Toolkit](https://github.com/isabelle-utp/Z_Toolkit)
-- [Shallow Expressions](https://github.com/isabelle-utp/Shallow-Expressions)
-- [Interaction Trees (robochart branch)](https://github.com/isabelle-utp/interaction-trees/tree/robochart)
-
-3. Create a `ROOTS` file in `/path/to/repos` with content below.
-```
-mirror-afp-2021/thys
-Z_Toolkit/
-Shallow-Expressions/
-Shallow-Expressions/Z/
-interaction-trees/
-```
-
-4. Load Isabelle/jedit
+# Animate RoboChart
+## Prebuild-image
+Load the theory `examples/RoboChart_basic_v1/RoboChart_basic_v1_1.thy` for animation, then move your cursor to a line `animate1 D_PatrolMod_p_sim` to animate. When the cursor stops there, code generator starts to generate Haskell code, and compile. Usually, we will see below on the `Output` window.
 ```
-$ /path/to/Isabelle2021/bin/isabelle jedit -d /path/to/repos
+See theory exports 
+Compiling animation... 
+See theory exports 
+Start animation
 ```
+Then click `Start animation`.
 
-# Animate RoboChart
+## Standard
 General steps are shown below. Please see instructions in each specific example for further considerations.
 
 1. Open the main theory file for a RoboChart model, such as `RoboChart_basic.thy` for the model in `examples/RoboChart_basic.thy/`
@@ -45,5 +33,3 @@ $ ghci main.hs
 $ ghc -g main.hs
 $ ./main
 ```
-
-Please note that we do have a customised Isabelle2021 version on which the animation process is very much simplified. All work is done in Isabelle. The only thing users need to do is to click an **animate1** command for animation, which will automatically export Haskell, compile into an executable, and then execute the animation on console of jedit. However, this particular version is for experiment only.

RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_Simulation.thy → RoboChart/RoboChart_Simulation.thy

@@ -12,9 +12,9 @@ begin
 generate_file \<open>code/simulate/Simulate.hs\<close> = \<open>
 module Simulate (simulate) where
 import Interaction_Trees;
-import Partial_Fun;
+import Prelude;
+-- import Partial_Fun;
 import System.IO;
-import qualified Data.List.Split;
 import qualified Data.List;
 
 -- These library functions help us to trim the "_C" strings from pretty printed events
@@ -29,7 +29,7 @@ removeSubstr w "" = "";
 removeSubstr w s@(c:cs) = (if w `isPrefixOf` s then Prelude.drop (Prelude.length w) s else c : removeSubstr w cs);
 
 replace :: String -> String -> String -> String;
-replace old new = Data.List.intercalate new . Data.List.Split.splitOn old;
+replace old new orig = orig;-- Data.List.intercalate new . old;
 
 renameGasEvent :: String -> String;
 renameGasEvent gas = 
@@ -117,12 +117,12 @@ structure ISim_Path = Theory_Data
 fun simulator_setup thy = 
   let open Isabelle_System; val tmp = Path.expand (create_tmp_path "itree-simulate" "")
   in case (ISim_Path.get thy) of NONE => () | SOME oldtmp => rm_tree oldtmp;
-    mkdir tmp; (tmp, ISim_Path.put (SOME tmp) thy)
+    make_directory tmp; (tmp, ISim_Path.put (SOME tmp) thy)
   end
 
-fun sim_files_cp tmp = 
+fun sim_files_cp ghc tmp = 
   "(fn path => let open Isabelle_System; val path' = Path.append path (Path.make [\"code\", \"simulate\"])" ^
-  " in writeln \"Compiling animation...\"; bash (\"cd \" ^ Path.implode path' ^ \"; ghc Simulation >> /dev/null\") ; copy_dir path' (Path.explode \"" ^ tmp ^ "\") end)"
+  " in writeln \"Compiling animation...\"; bash (\"cd \" ^ Path.implode path' ^ \"; " ^ ghc ^ " Simulation >> /dev/null\") ; copy_dir path' (Path.explode \"" ^ tmp ^ "\") end)"
 
 open Named_Target
 
@@ -139,6 +139,8 @@ fun prep_simulation model thy ctx =
   let open Generated_Files; 
       val (tmp, thy') = simulator_setup (Local_Theory.exit_global ctx);
       val ctx' = Named_Target.theory_init thy'
+      val ghc = getenv "ISABELLE_GHC"
+      val _ = if (ghc = "") then error "GHC is not set up. Please set the environment variable ISABELLE_GHC." else ()
   in
   generate_file (Path.binding0 (Path.make ["code", "simulate", "Simulation.hs"]), (Input.string (simulation_file model thy))) ctx' |>
   (fn ctx' => 
@@ -147,7 +149,7 @@ fun prep_simulation model thy ctx =
                  [([], (Local_Theory.exit_global ctx')), ([Path.binding0 (Path.make ["code", "simulate", "Simulate.hs"])], @{theory})] 
                  [] [([Path.binding0 (Path.make ["code", "simulate", "Simulation"])], SOME true)]
                  (Path.binding0 (Path.make []))
-                 (Input.string (sim_files_cp (Path.implode tmp)))
+                 (Input.string (sim_files_cp ghc (Path.implode tmp)))
     in ctx' end)
 
 
@@ -157,13 +159,13 @@ fun prep_simulation model thy ctx =
 fun run_simulation thy =
   case ISim_Path.get thy of
     NONE => error "No animation" |
-    SOME f => writeln (Active.run_system_shell_command (SOME (Path.implode f)) ("./Simulation") "Start animation")
+    SOME f => writeln (Active.run_system_shell_command (SOME (Path.implode f)) ("./simulate/Simulation") "Start animation")
 
 fun simulate model thy =
   let val ctx = Named_Target.theory_init thy
       val ctx' =
         (Code_Target.export_code true [Code.read_const (Local_Theory.exit_global ctx) model] [((("Haskell", ""), SOME ({physical = false}, (Path.explode "simulate", Position.none))), (Token.explode (Thy_Header.get_keywords' @{context}) Position.none "string_classes"))] ctx)
-        |> prep_simulation model (Context.theory_name thy)
+        |> prep_simulation model (Context.theory_name {long = false} thy)
   in run_simulation (Local_Theory.exit_global ctx'); (Local_Theory.exit_global ctx')
   end