Mercurial > hg > Gears > GearsAgda

comparison ModelChecking.agda @ 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
comparison
equal deleted inserted replaced
635:aee8de02dfe0 636:1c8dca459d9a
45 pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } ) 45 pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )
46 46
47 eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t 47 eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
48 eating p next = next p 48 eating p next = next p
49 49
50 data Code : Set where
51 C_set : Code
52 C_putdown_rfork : Code
53 C_putdown_lfork : Code
54 C_thinking : Code
55 C_pickup_rfork : Code
56 C_pickup_lfork : Code
57 C_eating : Code
58
59 record Process : Set where
60 field
61 phil : Phils
62 next : Code
63
64 putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
65 putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next = C_putdown_lfork } )
66
67 code_table : {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
68 code_table C_set = ?
69 code_table C_putdown_rfork = putdown_rfork_stub
70 code_table C_putdown_lfork = {!!}
71 code_table C_thinking = {!!}
72 code_table C_pickup_rfork = {!!}
73 code_table C_pickup_lfork = {!!}
74 code_table C_eating = {!!}
75
76 step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
77 step = {!!}
78
79
80
81