3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederCopyright : (c) Klaus Hartke, Uni Bremen 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederMaintainer : Christian.Maeder@dfki.de
f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederStability : experimental
f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederPortability : non-portable (MPTC-FD)
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule Kripke where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederKripke Structure
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------------- -}
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiclass Kripke k a s | k -> a s where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder states :: k -> Set s
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski initial :: k -> Set s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder next :: k -> s -> Set s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder labels :: k -> s -> Set a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ----------------------------------------------------------------------------