Mercurial > hg > Gears > GearsAgda

changeset 636:1c8dca459d9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Nov 2021 15:50:30 +0900
parents aee8de02dfe0
children e30dcd03c07f
files ModelChecking.agda
diffstat 1 files changed, 32 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Sun Nov 14 14:55:22 2021 +0900
+++ b/ModelChecking.agda	Sun Nov 14 15:50:30 2021 +0900
@@ -47,3 +47,35 @@
 eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
 eating p next = next  p 
 
+data Code : Set  where
+   C_set : Code
+   C_putdown_rfork : Code 
+   C_putdown_lfork : Code 
+   C_thinking : Code 
+   C_pickup_rfork : Code 
+   C_pickup_lfork : Code 
+   C_eating : Code 
+
+record Process : Set  where
+   field
+      phil : Phils
+      next : Code 
+
+putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
+putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next = C_putdown_lfork } )
+
+code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
+code_table C_set  = ?
+code_table C_putdown_rfork = putdown_rfork_stub
+code_table C_putdown_lfork = {!!}
+code_table C_thinking = {!!}
+code_table C_pickup_rfork = {!!}
+code_table C_pickup_lfork = {!!}
+code_table C_eating = {!!}
+
+step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
+step = {!!}
+
+
+
+