Updated the animator and checking tools to properly handle outputs. T…

…he Z-Machine animator now expects the IO form explicitly, and so cannot be applied to arbitrary Circus processes.
isabelle-utp · Jul 3, 2024 · c7cb3a3 · c7cb3a3
1 parent 6f9d682
commit c7cb3a3
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 34 deletions.
diff --git a/Z_Animator.thy b/Z_Animator.thy
@@ -22,15 +22,15 @@ removeSubstr :: String -> String -> String;
 removeSubstr w "" = "";
 removeSubstr w s@(c:cs) = (if w `isPrefixOf` s then Prelude.drop (Prelude.length w) s else c : removeSubstr w cs);
 
-data EventCont p = InputEvtCont [(String, p)] | OutEvtCont (String, p)
+data EventCont p = MultiEvtCont [(String, p)] | SingleEvtCont (String, p)
 
 showEventCont :: (String, EventCont p) -> String
-showEventCont (n, InputEvtCont _) = n
-showEventCont (n, OutEvtCont (v, _)) = n ++ " " ++ v
+showEventCont (n, MultiEvtCont _) = n
+showEventCont (n, SingleEvtCont (v, _)) = n ++ " " ++ v
 
 eventHierarchy :: [(String, p)] -> [(String, EventCont p)]
 eventHierarchy m = map (\c -> (c,
-                              (\es -> if length es == 1 then OutEvtCont (head es) else InputEvtCont es)
+                              (\es -> if length es == 1 then SingleEvtCont (head es) else MultiEvtCont es)
                               $ map (\(e, p) -> (tail (dropWhile (\x -> x /= ' ') e), p)) 
                               $ filter (isPrefixOf (c ++ " ") . fst) m)) chans
   where
@@ -48,30 +48,35 @@ animate_cnt n (Sil p) =
 animate_cnt n (Vis (Pfun_of_alist [])) = putStrLn "Deadlocked.";
 animate_cnt n t@(Vis (Pfun_of_alist m)) = 
   do { putStrLn ("Operations:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map showEventCont eh))));
+       putStr ("Choose [1-" ++ show (length eh) ++ "]: ");
        e <- getLine;
        if (e == "q" || e == "Q") then
          putStrLn "Animation terminated"
        else
        case (reads e) of
-         []       -> do { putStrLn "No parse"; animate_cnt n t }
-         [(v, _)] -> if (v > length eh)
-                       then do { putStrLn "Rejected"; animate_cnt n t }
-                       else case (snd (eh !! (v - 1))) of
-                              InputEvtCont opts -> 
-                                do { putStrLn ("Parameters:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map fst opts))))
-                                   ; e <- getLine
-                                   ; case (reads e) of
-                                       []       -> do { putStrLn "No parse"; animate_cnt n t }
-                                       [(v, _)] -> if (v > length opts)
-                                                   then do { putStrLn "Rejected"; animate_cnt n t }
-                                                   else animate_cnt 0 (snd (opts !! (v - 1)))
-
-                                   }
-                              OutEvtCont (_, p) -> animate_cnt 0 p
+         []       -> do { putStrLn "Invalid choice, try again."; animate_cnt n t }
+         [(v, _)] -> 
+           if (v > length eh)
+           then do { putStrLn "Rejected"; animate_cnt n t }
+           else case (snd (eh !! (v - 1))) of
+                  MultiEvtCont opts -> 
+                    do { putStrLn ("Parameters:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map fst opts))))
+                       ; putStr ("Choose [1-" ++ show (length opts) ++ "]: ")
+                       ; e <- getLine
+                       ; case (reads e) of
+                           []       -> do { putStrLn "No parse"; animate_cnt n t }
+                           [(v, _)] -> if (v > length opts)
+                                       then do { putStrLn "Rejected"; animate_cnt n t }
+                                       else case snd (opts !! (v - 1)) of 
+                                              Vis (Pfun_of_alist [(e, p')]) -> 
+                                                do { putStrLn ("Response: " ++ show e); putStrLn ""; animate_cnt 0 p' }   
+  
+                       }
+                  SingleEvtCont (_, Vis (Pfun_of_alist [(e, p')])) -> do { putStrLn ("Response: " ++ show e); putStrLn ""; animate_cnt 0 p' }
      }                                                            
   where eh = eventHierarchy (map (\(e, p) -> (Prelude.show e, p)) m);
 animate :: (Eq e, Prelude.Show e, Prelude.Show s) => Itree e s -> Prelude.IO ();
-animate p = do { hSetBuffering stdout NoBuffering; putStrLn ""; putStrLn "Starting Animation..."; animate_cnt 0 p }
+animate p = do { hSetBuffering stdout NoBuffering; putStrLn ""; putStrLn "Starting Animation..."; putStrLn ""; animate_cnt 0 p }
 \<close>
 
 ML \<open> 

diff --git a/Z_Machine.ML b/Z_Machine.ML
@@ -52,7 +52,7 @@ fun mk_chan_show_fun tname ops ctx =
   let val typ = Syntax.read_typ ctx tname in
   Function_Fun.add_fun 
     [(Binding.name ("show_" ^ tname), SOME (typ --> @{typ "String.literal"}), NoSyn)]
-    (map (fn n => ((Binding.empty_atts, mk_chan_show_eq n ctx), [], [])) (ops @ map (fn n => n ^ "Out") ops))
+    (map (fn n => ((Binding.empty_atts, mk_chan_show_eq n ctx), [], [])) (ops @ map (fn n => n ^ "_Out") ops))
     (Function_Fun.fun_config) ctx
   end
 
@@ -196,7 +196,7 @@ fun zmachine_body_sem n st init inve ops ends ctx =
   let open Syntax; open HOLogic; open Proof_Context
       val oplist = 
             mk_list dummyT 
-              (map (fn n => const @{const_name zop_event} $ read_const {proper = false, strict = false} ctx (firstLower n) $ const (read_const_name ctx (zop_type n)) $ read_const {proper = false, strict = false} ctx (firstLower n ^ "Out") $  const (read_const_name ctx n)) ops)
+              (map (fn n => const @{const_name zop_event} $ read_const {proper = false, strict = false} ctx (firstLower n) $ const (read_const_name ctx (zop_type n)) $ read_const {proper = false, strict = false} ctx (firstLower n ^ "_Out") $  const (read_const_name ctx n)) ops)
   in snd (Local_Theory.define 
            ((Binding.name n, NoSyn)
          , ((Binding.name (n ^ "_def")
@@ -209,7 +209,7 @@ fun chantype_name n = n ^ "_chan"
 fun zmachine_sem (ZMachine {name = n, state = s, init = i, inv = inv, operations = ops, ends = e}) ctx =
   let open Syntax; open HOLogic; open Lift_Expr
     val cs = map (fn n => (firstLower n, YXML.content_of (string_of_typ ctx (get_zop_ptype n ctx)))) ops @
-             map (fn n => (firstLower n ^ "Out", YXML.content_of (string_of_typ ctx (get_zop_outtype n ctx)))) ops
+             map (fn n => (firstLower n ^ "_Out", YXML.content_of (string_of_typ ctx (get_zop_outtype n ctx)))) ops
     val st = read_typ ctx s
     val inve = mk_lift_expr ctx (parse_term ctx inv)
     val init = parse_term ctx i

diff --git a/Z_Testing.thy b/Z_Testing.thy
@@ -60,14 +60,14 @@ test_event n t p = do { case trs of
                         [] -> putStrLn ("No matching traces found of length <= " ++ show n ++ ".")
                         (tr : _) -> putStrLn ("Trace found: " ++ show tr ++ ".")
                     }
-  where trs = event_traces n t p
+  where trs = event_traces (n * 2) t p
 
 test_dlock :: Show e => Int -> Itree e s -> IO ()
 test_dlock n p = do { case trs of
                         [] -> putStrLn ("No deadlocking traces found of length <= " ++ show n ++ ".")
                         (tr : _) -> putStrLn ("Deadlocks after: " ++ show tr ++ ".")
                     }
-  where trs = dlock_traces n p
+  where trs = dlock_traces (n * 2) p
 \<close>
 
 

diff --git a/examples/Buffer_Z.thy b/examples/Buffer_Z.thy
@@ -4,28 +4,28 @@ theory Buffer_Z
   imports "Z_Machines.Z_Machine"
 begin lit_vars
 
-consts VAL :: "integer set"
+consts VAL :: "int set"
 
 zstore Buffer_state =
-  buf :: "integer list"
+  buf :: "int list"
+  v :: "int"
   where "set buf \<subseteq> VAL"
 
 zoperation Input =
   over Buffer_state
-  params v \<in> VAL
-  update "[buf \<leadsto> buf @ [v]]"
+  params x \<in> VAL
+  update "[buf \<leadsto> buf @ [x]]"
 
-lemma Input_inv [hoare_lemmas]: "Input v preserves Buffer_state_inv"
+lemma Input_inv [hoare_lemmas]: "Input x preserves Buffer_state_inv"
   by zpog_full
 
 zoperation Output =
   over Buffer_state
-  params v \<in> VAL
   pre "length buf > 0"
-  update "[buf \<leadsto> tl buf]"
-  where "v = hd buf"
+  update "[buf \<leadsto> tl buf, v \<leadsto> hd buf]"
+  output v
 
-lemma Output_inv [hoare_lemmas]: "Output v preserves Buffer_state_inv"
+lemma Output_inv [hoare_lemmas]: "Output() preserves Buffer_state_inv"
   by zpog_full (meson in_mono list.set_sel(2))
 
 zoperation State =