{-|
Module   : ExampleRevelation
Description :
ExampleRevelation> sat predicate'
Unsatisfiable
ExampleRevelation> sat predicate
Satisfiable. Model:
  x = False :: Bool
  h =  True :: Bool
ExampleRevelation> sat predicateSP
Satisfiable. Model:
  x = True :: Bool
  h = True :: Bool
-}
module ExampleRevelation (predicate, predicate', predicateSP) where
import Data.SBV
import Logics
import Translation
import ToSBV

ag = Agent {identity=0, nonobs=[BVar "h"]} -- h is not observed by ag

-- | Variables
varx = BVar "x" 
valx = BValue (BVar "x") 

varh = BVar "h" 
valh = BValue (BVar "h") 

allVars :: [Var] 
allVars = [varx, varh] 

-- | Context
phi = true

-- | Program  x:=h
prog = BAssign varx valh

-- | Box formula [x:=h] (K_ag h)   -- satisfiability (x=F, h=T) (x=T, h=T) --> (x=T, h=T)    
alpha :: ModalFormula
alpha = Box prog (K ag (Atom valh))
-- alpha = Box prog ((Atom valh))

-- | Box formula K_ag ([x:=h] h)   -- unsat
alpha' :: ModalFormula
alpha' = K ag (Box prog (Atom valh))

-- | the predicate used as input in SBV
predicate = toSBV allVars phi (tau phi alpha)
predicate' = toSBV allVars phi (tau phi alpha')

-- | check alpha with the SP translation method
predicateSP = toSBV allVars (sp phi prog) (tau (sp phi prog) (alpha))