Kripke.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuModule : $EmptyHeader$
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuDescription : <optional short description entry>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuCopyright : (c) <Authors or Affiliations>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuLicense : GPLv2 or higher
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuMaintainer : <email>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuStability : unstable | experimental | provisional | stable | frozen
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuPortability : portable | non-portable (<reason>)
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu<optional description>
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski{-# OPTIONS -fglasgow-exts #-}
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule Kripke where
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski{------------------------------------------------------------------------------}
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski{- Kripke Structure -}
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski{------------------------------------------------------------------------------}
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiclass Kripke k a s | k -> a s where
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski states :: k -> Set s
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski initial :: k -> Set s
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski next :: k -> s -> Set s
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski labels :: k -> s -> Set a
26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski{------------------------------------------------------------------------------}