Bachelor thesis: "Verbesserte SMT-basierte Verifikation von SCADE-Modellen mit LAMA"

example/Switch-coinduction.smt

@@ -0,0 +1,156 @@
+;; Implementation of Switch.lm by hand for exploration
+;; Proves the 3 given properties using (0-)coinduction.
+;; There are slight variants (commented) of those
+;; properties which are incorrect. Those give the
+;; expected counterexamples.
+
+;; node Switch
+(define-fun Switch_s_def ((on Bool) (off Bool) (s_1 Bool) (s Bool)) Bool
+  (= s
+     (ite s_1 (not off) on)))
+(define-fun Switch_s_1_def ((s Bool) (s_1_next Bool)) Bool
+  (= s_1_next
+     s ))
+(define-fun Switch_so_def ((so Bool) (s Bool)) Bool
+  (= so
+     s))
+
+;; Global flow
+(define-fun Switch_on_def ((Switch_on Bool) (on Bool)) Bool
+  (= Switch_on
+     on))
+(define-fun Switch_off_def ((Switch_off Bool) (off Bool)) Bool
+  (= Switch_off
+     off))
+(define-fun s_def ((Switch_so Bool) (s Bool)) Bool
+  (= s
+     Switch_so))
+(define-fun s_1_def ((s_1_next Bool) (s Bool)) Bool
+  (= s_1_next
+     s))
+
+;; properties
+(define-fun prop1 ((off Bool) (on Bool) (s Bool)) Bool
+;  (=> on s))
+  (=> (and on (not off)) s))
+(define-fun prop2 ((off Bool) (on Bool) (s Bool)) Bool
+;  (=> off (not s)))
+  (=> (and off (not on)) (not s)))
+(define-fun prop3 ((off Bool) (on Bool) (s Bool) (s_1 Bool)) Bool
+  (=> (and (not off) (not on)) (= s s_1)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Prove that initial state fulfils property
+
+(push)
+
+;; declarations
+(declare-fun Switch_on_0 () Bool)
+(declare-fun Switch_off_0 () Bool)
+(declare-fun Switch_so_0 () Bool)
+(declare-fun Switch_s_0 () Bool)
+(declare-fun Switch_s_1_0 () Bool)
+
+(declare-fun on_0 () Bool)
+(declare-fun off_0 () Bool)
+(declare-fun s_0 () Bool)
+(declare-fun s_1_0 () Bool)
+
+(declare-fun Switch_s_1_1 () Bool)
+(declare-fun s_1_1 () Bool)
+
+;; initialisation
+(assert (= Switch_s_1_0 false))
+(assert (= s_1_0 false))
+
+(assert (Switch_on_def Switch_on_0 on_0))
+(assert (Switch_off_def Switch_off_0 off_0))
+
+(assert (Switch_so_def Switch_so_0 Switch_s_0))
+(assert (Switch_s_def Switch_on_0 Switch_off_0 Switch_s_1_0 Switch_s_0))
+(assert (Switch_s_1_def Switch_s_0 Switch_s_1_1))
+
+(assert (s_def s_0 Switch_so_0))
+(assert (s_1_def s_1_1 s_0))
+
+;(assert (not (prop1 off_0 on_0 s_0)))
+(assert (not (prop2 off_0 on_0 s_0)))
+;(assert (not (prop3 off_0 on_0 s_0 s_1_0)))
+
+(check-sat)
+(get-model)
+(pop)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Prove that property is an invariant
+
+;; declarations
+(declare-fun Switch_on () Bool)
+(declare-fun Switch_off () Bool)
+(declare-fun Switch_so () Bool)
+(declare-fun Switch_s () Bool)
+(declare-fun Switch_s_1 () Bool)
+
+(declare-fun on () Bool)
+(declare-fun off () Bool)
+(declare-fun s () Bool)
+(declare-fun s_1 () Bool)
+
+(declare-fun Switch_s_1_n1 () Bool)
+(declare-fun s_1_n1 () Bool)
+
+(declare-fun Switch_on_n1 () Bool)
+(declare-fun Switch_off_n1 () Bool)
+(declare-fun Switch_so_n1 () Bool)
+(declare-fun Switch_s_n1 () Bool)
+
+(declare-fun on_n1 () Bool)
+(declare-fun off_n1 () Bool)
+(declare-fun s_n1 () Bool)
+
+(declare-fun Switch_s_1_n2 () Bool)
+(declare-fun s_1_n2 () Bool)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Assume that we start in a state in which the invariant holds
+
+;(assert (prop1 off on s))
+(assert (prop2 off on s))
+;(assert (prop3 off on s s_1))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Set up variables in starting state
+
+(assert (Switch_on_def Switch_on on))
+(assert (Switch_off_def Switch_off off))
+
+(assert (Switch_so_def Switch_so Switch_s))
+(assert (Switch_s_def Switch_on Switch_off Switch_s_1 Switch_s))
+(assert (Switch_s_1_def Switch_s Switch_s_1_n1))
+
+(assert (s_def s Switch_so))
+(assert (s_1_def s_1_n1 s))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Make transition
+
+(assert (Switch_on_def Switch_on_n1 on_n1))
+(assert (Switch_off_def Switch_off_n1 off_n1))
+
+(assert (Switch_so_def Switch_so_n1 Switch_s_n1))
+(assert (Switch_s_def Switch_on_n1 Switch_off_n1 Switch_s_1_n1 Switch_s_n1))
+(assert (Switch_s_1_def Switch_s_n1 Switch_s_1_n2))
+
+(assert (s_def s_n1 Switch_so_n1))
+(assert (s_1_def s_1_n2 s_n1))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Try to prove that property holds after transition
+(push)
+;(assert (not (prop1 off_n1 on_n1 s_n1)))
+(assert (not (prop2 off_n1 on_n1 s_n1)))
+;(assert (not (prop3 off_n1 on_n1 s_n1 s_1_n1)))
+
+(check-sat)
+(get-model)
+(pop)

interpreter/LAMA.cabal

@@ -8,7 +8,7 @@ Description:
 Executable test-lama
   default-language: Haskell2010
   build-depends: base, containers, mtl, bytestring, natural-numbers,
-    transformers, pretty, array, HUnit, language-lama
+    transformers, pretty, array, HUnit, language-lama, fgl >= 5.5.0.0
   hs-source-dirs: test lib
   GHC-Options: -Wall
   other-modules:

interpreter/Main.hs

@@ -18,7 +18,6 @@ import Data.Foldable (forM_, foldlM, foldl)
 import Lang.LAMA.Identifier
 import qualified Data.Map as Map
 import Data.Map (Map)
-import Data.Graph.Inductive.GenShow ()
 import Control.Monad (void, when, MonadPlus(..))
 import Control.Monad.Trans.Maybe
 import Control.Monad.IO.Class

lamaSMT/LamaSMT.cabal

@@ -1,5 +1,5 @@
 Name:           LamaSMT
-Version:        0.1
+Version:        0.3
 Build-Type:     Simple
 Cabal-Version:  >= 1.10
 Description:
@@ -15,4 +15,4 @@ Executable lamasmt
   GHC-Options: -Wall -rtsopts
   other-modules:
     Transform
-  Main-Is: Main.hs
+  Main-Is: Main.hs

lamaSMT/Main.hs

@@ -5,10 +5,8 @@ module Main (main) where
 
 import qualified Data.ByteString.Lazy.Char8 as BL
 
-import Text.PrettyPrint (render)
+import Text.PrettyPrint (Doc, render, vcat, text, ($$))
 import Data.List.Split (splitOn)
-import Data.List (intercalate)
-import Data.Natural
 
 import System.IO (stdin)
 import System.Environment (getArgs)
@@ -170,7 +168,7 @@ run opts@Options{..} file inp = do
   model <- runCheck opts
     ( (liftSMT $ mapM_ setOption optSMTOpts) >>
       lamaSMT optNatImpl optEnumImpl p >>=
-      (uncurry $ checkWithModel optNatImpl optStrategy) )
+      (uncurry $ checkWithModel optStrategy) )
   liftIO $ checkModel opts p model
 
 checkErrors :: Either Error a -> MaybeT IO a
@@ -204,11 +202,36 @@ runCheck progOpts = chooseSolver progOpts . checkError
                       -- ++ solverBase
   -- withPipe solverCmd []
 
-checkModel :: Ident i => Options -> Program i -> Maybe (Natural, Model i) -> IO ()
-checkModel _ _ Nothing = putStrLn "42"
-checkModel opts prog (Just (lastIndex, m)) =
+checkModel :: Ident i =>
+           Options
+           -> Program i
+           -> (StrategyResult i)
+           -> IO ()
+checkModel _ _ Success = putStrLn "42"
+checkModel opts prog (Failure lastIndex m) =
   do putStrLn ":-("
+     putStrLn $ "Found counterexample at depth " ++ show lastIndex
      when (optDumpModel opts) (putStrLn . render $ prettyModel m)
      case optScenarioFile opts of
        Nothing -> return ()
-       Just f -> writeFile f $ render $ scadeScenario prog (optTopNodePath opts) lastIndex m
+       Just f -> writeFile f $ render $ scadeScenario prog (optTopNodePath opts) m
+checkModel opts prog (Unknown what hints) =
+  do putStrLn ":-("
+     putStrLn what
+     when (optDumpModel opts)
+          (putStrLn . render . prettyHints $ hints)
+     case optScenarioFile opts of
+       Nothing -> return ()
+       Just f ->
+         mapM_ (\h ->
+                 writeFile (f ++ "_" ++ hintDescr h)
+                 . render
+                 $ scadeScenario prog (optTopNodePath opts) (hintModel h))
+               hints
+
+prettyHints :: Ident i => Hints i -> Doc
+prettyHints = vcat . map prettyHint
+  where
+    prettyHint h
+      = text ("Hint for " ++ (hintDescr h))
+        $$ prettyModel (hintModel h)

lamaSMT/lib/Check.hs

@@ -3,4 +3,4 @@ module Check where
 import Strategy
 
 check :: Strategy s => 
-check = undefined
+check = undefined

lamaSMT/lib/Definition.hs

@@ -1,31 +1,36 @@
 module Definition where
 
-import Data.Array as Arr
-
 import Language.SMTLib2 as SMT
 
+import Data.Array as Arr
+
 import LamaSMTTypes
 import Internal.Monads
 
 data Definition =
-  SingleDef (Stream Bool)
+  SingleDef [Int] Bool (SMTFunction [TypedExpr] Bool)
   | ProdDef (Array Int Definition)
---  deriving Show
+  deriving Show
 
-ensureDefinition :: TypedStream i -> Definition
-ensureDefinition (BoolStream s) = SingleDef s
-ensureDefinition (ProdStream ps) = ProdDef $ fmap ensureDefinition ps
-ensureDefinition _
-  = error $ "ensureDefinition: not a boolean stream" -- : " ++ show s
+ensureDefinition :: [Int] -> Bool -> TypedFunc -> Definition
+ensureDefinition argN succ (BoolFunc s) = SingleDef argN succ s
+ensureDefinition argN succ (ProdFunc ps) = ProdDef $ fmap (ensureDefinition argN succ) ps
+ensureDefinition _ _ _
+  = error $ "ensureDefinition: not a boolean function"
 
 assertDefinition :: MonadSMT m =>
                     (SMTExpr Bool -> SMTExpr Bool)
-                    -> StreamPos
+                    -> ([TypedExpr], [TypedExpr])
                     -> Definition
                     -> m ()
-assertDefinition f i (SingleDef s) = liftSMT $ assert (f $ s `app` i)
+assertDefinition f i (SingleDef argN succ s) = liftSMT $ assert (f $ s `app` (lookupArgs argN succ i))
 assertDefinition f i (ProdDef ps) = mapM_ (assertDefinition f i) $ Arr.elems ps
 
+lookupArgs :: [Int] -> Bool -> ([TypedExpr], [TypedExpr])
+               -> [TypedExpr]
+lookupArgs argN True vars = [(snd vars) !! (head argN)] ++ (map ((!!) (fst vars)) $ tail argN)
+lookupArgs argN False vars = map ((!!) (fst vars)) argN
+
 data ProgDefs = ProgDefs
                 { flowDef :: [Definition]
                 , precondition :: Definition

lamaSMT/lib/Internal/Monads.hs

@@ -6,6 +6,7 @@ import Control.Monad.Error
 import Control.Monad.State.Lazy as Lazy
 import Control.Monad.State.Strict as Strict
 import Control.Monad.Reader
+import Control.Monad.Writer
 
 -- | Lift an SMT action into an arbitrary monad (like liftIO).
 class Monad m => MonadSMT m where
@@ -25,3 +26,6 @@ instance MonadSMT m => MonadSMT (Strict.StateT s m) where
 
 instance MonadSMT m => MonadSMT (ReaderT r m) where
   liftSMT = lift . liftSMT
+
+instance (Monoid w, MonadSMT m) => MonadSMT (WriterT w m) where
+  liftSMT = lift . liftSMT