@@ -36,6 +36,13 @@ data RegState = RegState
3636 deriving (Show , Generic )
3737
3838deriving instance Show (Action RegState a )
39+ deriving instance Eq (Action RegState a )
40+
41+ instance HasVariables (Action RegState a ) where
42+ getAllVariables (Register _ v) = getAllVariables v
43+ getAllVariables (KillThread v) = getAllVariables v
44+ getAllVariables (Successful a) = getAllVariables a
45+ getAllVariables _ = mempty
3946
4047instance StateModel RegState where
4148 data Action RegState a where
@@ -157,6 +164,20 @@ positive s (Unregister name) =
157164 name `Map.notMember` regs s
158165positive _s _ = True
159166
167+ data ShowDict s a where
168+ ShowDict :: Show (Realized (RegM s ) a ) => ShowDict s a
169+
170+ showDictAction :: forall s a . Action RegState a -> ShowDict s a
171+ showDictAction Spawn {} = ShowDict
172+ showDictAction WhereIs {} = ShowDict
173+ showDictAction Register {} = ShowDict
174+ showDictAction Unregister {} = ShowDict
175+ showDictAction KillThread {} = ShowDict
176+ showDictAction (Successful a) = showDictAction a
177+
178+ tabu :: String -> [String ] -> Property -> Property
179+ tabu tab xs = tabulate tab xs . foldr (.) id [classify True (tab ++ " : " ++ x) | x <- xs]
180+
160181instance DynLogicModel RegState where
161182 restricted (Successful _) = True
162183 restricted _ = False
@@ -184,9 +205,6 @@ shrinkName name = [n | n <- allNames, n < name]
184205allNames :: [String ]
185206allNames = [" a" , " b" , " c" , " d" , " e" ]
186207
187- tabu :: String -> [String ] -> Property -> Property
188- tabu tab xs = tabulate tab xs . foldr (.) id [classify True (tab ++ " : " ++ x) | x <- xs]
189-
190208prop_Registry :: Actions RegState -> Property
191209prop_Registry s =
192210 property $
@@ -290,15 +308,4 @@ tests =
290308 , testProperty " canRegisterNoUnregister" $ expectFailure $ propDL canRegisterNoUnregister
291309 ]
292310
293- data ShowDict s a where
294- ShowDict :: Show (Realized (RegM s ) a ) => ShowDict s a
295-
296- showDictAction :: forall s a . Action RegState a -> ShowDict s a
297- showDictAction Spawn {} = ShowDict
298- showDictAction WhereIs {} = ShowDict
299- showDictAction Register {} = ShowDict
300- showDictAction Unregister {} = ShowDict
301- showDictAction KillThread {} = ShowDict
302- showDictAction (Successful a) = showDictAction a
303311
304- makeActionInstances ''RegState
0 commit comments