lattest-lib-0.1.0.0: test/Test/Lattest/Model/STSTest.hs
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE LambdaCase #-}
module Test.Lattest.Model.STSTest (
testSTSHappyFlow,
testSTSHappyFlowFloat,
testLatticeCoffeeSTS,
testErrorThrowingGates,
testSTSUnHappyFlow,
testPrintSTS,
testSTSTestSelection,
testLatticeSTS,
testLatticeSTSQuiescence
)
where
import Prelude hiding (take)
import Test.HUnit
import Data.Maybe(fromJust)
import qualified Data.Set as Set
import System.Random(mkStdGen)
import Data.String(IsString)
import qualified Text.RawString.QQ as QQ
import qualified Lattest.Adapter.Adapter as Adapter
import Lattest.Adapter.StandardAdapters(pureAdapter)
import Lattest.Exec.StandardTestControllers
import Lattest.Exec.Testing(runSMTTester, Verdict(..))
import Lattest.Model.Automaton(after, stateConf,automaton,IntrpState(..),prettyPrintIntrp,stsTLoc)
import Lattest.Model.StandardAutomata(interpretSTS, IOSTS, STSIntrp, interpretSTSQuiescentInputAttemptConcrete)
import Lattest.Model.Alphabet(IOAct(..), Suspended(..), SuspendedIF, SuspendedIFGateValue, δ, SymInteract(..),GateValue(..), gateValueAsIOAct,toIOGateValue, InputAttempt(..))
import Lattest.Model.BoundedMonad(Det, (/\), (\/), underspecified, forbidden, FreeLattice, atom, disjunction)
import Reference.FreeLatticeSlow(FreeLatticeSlow)
import qualified Data.Map as Map
import qualified Control.Exception as Exception
import Lattest.Model.Symbolic.Expr
import qualified Lattest.SMT as SMT
pvar :: Variable
pvar = (Variable "p" IntType)
qvar :: Variable
qvar = (Variable "q" IntType)
xvar :: Variable
xvar = (Variable "x" IntType)
stsExampleInitAssign :: Valuation
stsExampleInitAssign = fromConstantsMap $ Map.singleton xvar (Cint 0)
stsExample :: IOSTS Det Integer String String
stsExample =
let p = sVar pvar :: Expr Integer
x = sVar xvar :: Expr Integer
water = SymInteract (In "water") [pvar]
ok = SymInteract (Out "ok") [pvar]
coffee = SymInteract (Out "coffee") []
waterGuard = 1 .<= p .&& p .<= 10
waterAssign = assignment [xvar =: x .+ p]
okGuard = x .== p
coffeeGuard = x .>= 15
initConf = return 0
switches = \q -> case q of
0 -> Map.fromList [(water, pure (stsTLoc waterGuard waterAssign, 1)),
(coffee, pure (stsTLoc coffeeGuard noAssignment, 2))]
1 -> Map.fromList [(ok, pure (stsTLoc okGuard noAssignment, 0))]
2 -> Map.empty
in automaton initConf (Set.fromList [water,ok,coffee]) switches
stsExampleIntrpr :: STSIntrp Det Integer (IOAct String String)
stsExampleIntrpr = interpretSTS stsExample stsExampleInitAssign
getSTSIntrpState :: Integer -> Integer -> Det (IntrpState Integer)
getSTSIntrpState loc val = pure $ IntrpState loc $ fromConstantsMap $ Map.singleton (Variable "x" IntType) (Cint val)
testSTSHappyFlow :: Test
testSTSHappyFlow = TestCase $ do
assertEqual "\ninitial state " (getSTSIntrpState 0 0) (stateConf stsExampleIntrpr)
let intrp2 = after stsExampleIntrpr (GateValue (In "water") [Cint 7])
assertEqual "after water 7: " (getSTSIntrpState 1 7) (stateConf intrp2)
let intrp3 = after intrp2 (GateValue (Out "ok") [Cint 7])
assertEqual "after ok 7: " (getSTSIntrpState 0 7) (stateConf intrp3)
let intrp4 = after intrp3 (GateValue (In "water") [Cint 9])
assertEqual "after water 9: " (getSTSIntrpState 1 16) (stateConf intrp4)
let intrp5 = after intrp4 (GateValue (Out "ok") [Cint 16])
assertEqual "after ok 16: " (getSTSIntrpState 0 16) (stateConf intrp5)
let intrp6 = after intrp5 (GateValue (Out "coffee") [])
assertEqual "after coffee: " (getSTSIntrpState 2 16) (stateConf intrp6)
return()
testErrorThrowingGates :: Test
testErrorThrowingGates = TestCase $ do
let intrp1 = after stsExampleIntrpr (GateValue (Out "water") [Cint 7])
assertThrowsError "gate not in STS alphabet" (stateConf intrp1)
let intrp2 = after stsExampleIntrpr (GateValue (In "water") [])
assertThrowsError "nr of values unequal to nr of parameters: 0 values and 1 variables" (stateConf intrp2)
let intrp3 = after stsExampleIntrpr (GateValue (In "water") [Cbool True])
assertThrowsError "type of variable and value do not match. Variables: [p:Int], Values: [True]" (stateConf intrp3)
testSTSUnHappyFlow :: Test
testSTSUnHappyFlow = TestCase $ do
let intrp3 = after stsExampleIntrpr (GateValue (Out "ok") [Cint 0]) -- output not enabled
assertEqual "after ok: " forbidden (stateConf intrp3)
let intrp4 = after stsExampleIntrpr (GateValue (In "water") [Cint 11]) -- value for input does not satisfy guard
assertEqual "after water 11: " underspecified (stateConf intrp4)
let intrp5 = after stsExampleIntrpr (GateValue (Out "coffee") []) -- value of variable does not satisfy guard
assertEqual "after coffee: " forbidden (stateConf intrp5)
assertThrowsError :: String -> a -> IO ()
assertThrowsError expectedError someVal = do
actualError <- Exception.handle handler $ do
_ <- Exception.evaluate someVal
return Nothing -- no exception thrown, so no error message
assertEqual "expected error: " (Just expectedError) actualError
where
handler :: Exception.ErrorCall -> IO (Maybe String)
handler ex = return $ Just $ show ex
testPrintSTS :: Test
testPrintSTS = TestCase $ assertBool failureMessage (expected == actual) -- no assertEquals to avoid printing the unreadable ascii-escaped variant of the tested unicode strings
where
failureMessage = "print of STS does not match, expected:" ++ expected ++ "but received:" ++ actual
actual = "\n" ++ prettyPrintIntrp stsExampleIntrpr ++ "\n" -- newlines before and after to match those of the "expected" below.
-- fancy quasiquotes to allow direct copy-pasting of the printed expected string into the source code below. With newline at start and end for readability.
expected = [QQ.r|
current state configuration: (0,{x:=0})
initial location configuration: 0
locations: 0, 1, 2
transitions:
0 ――?"water" [p:Int]⟶ ((((-p+10)) ≥ 0)∧(((p+-1)) ≥ 0), {x:=(p+x)},1)
0 ――!"coffee" []⟶ (((x+-15)) ≥ 0, {},2)
0 ――!"ok" [p:Int]⟶ -forbidden-
1 ――?"water" [p:Int]⟶ -underspecified-
1 ――!"coffee" []⟶ -forbidden-
1 ――!"ok" [p:Int]⟶ ((x) = (p), {},0)
2 ――?"water" [p:Int]⟶ -underspecified-
2 ――!"coffee" []⟶ -forbidden-
2 ――!"ok" [p:Int]⟶ -forbidden-
|]
data ImpExampleLoc = L0 | L1 | L2 deriving (Eq, Ord, Show)
-- TODO the "x" here is not implemented properly, it should be something like "xvar = (Variable "x" IntType)", see the example at the top of this file
tExampleCorrect :: (Ord i, Ord o, IsString i, IsString o) => (ImpExampleLoc, Integer) -> Map.Map (GateValue (IOAct i o)) (ImpExampleLoc, Integer)
tExampleCorrect (L0, x) = Map.fromList $
[((GateValue (In "water") [Cint p]), (L1, x+p)) | p <- [1..10]] ++ [((GateValue (Out "coffee") []), (L2, 0)) | x > 15]
tExampleCorrect (L1, x) = Map.fromList $ [((GateValue (Out "ok") [Cint x]), (L0, x))]
tExampleCorrect (L2, _) = Map.fromList $ []
impExampleCorrect :: IO (Adapter.Adapter (SuspendedIFGateValue String String) (Maybe (GateValue String)))
impExampleCorrect = do
imp <- pureAdapter (mkStdGen 123) 0.5 (Map.mapKeys gateValueAsIOAct <$> tExampleCorrect) (L0, 0) :: IO (Adapter.Adapter (SuspendedIF (GateValue String) (GateValue String)) (Maybe (GateValue String)))
Adapter.mapActionsFromSut toIOGateValue imp
testSTSTestSelection :: Test
testSTSTestSelection = TestCase $ do
let nrSteps = 37
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.05 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impExampleCorrect
(verdict, ((observed, _), _)) <- runSMTTester (interpretSTSQuiescentInputAttemptConcrete stsExample stsExampleInitAssign) testSelector imp
let checkObserved = go 0 0 observed
let exampleObserved = [
inp "water" [Cint 1],
out "ok" [Cint 1],
inp "water" [Cint 1],
out "ok" [Cint 2],
GateValue δ [],
inp "water" [Cint 1],
out "ok" [Cint 3],
inp "water" [Cint 1],
outL "ok" [Cint 4],
inpL "water" [Cint 1],
outL "ok" [Cint 5],
GateValue δ [],
inpL "water" [Cint 1],
outL "ok" [Cint 6],
inpL "water" [Cint 1],
outL "ok" [Cint 7],
inpL "water" [Cint 1],
outL "ok" [Cint 8],
inpL "water" [Cint 1],
outL "ok" [Cint 9],
inpL "water" [Cint 1],
outL "ok" [Cint 10],
inpL "water" [Cint 1],
outL "ok" [Cint 11],
inpL "water" [Cint 1],
outL "ok" [Cint 12],
inpL "water" [Cint 1],
outL "ok" [Cint 13],
inpL "water" [Cint 1],
outL "ok" [Cint 14],
inpL "water" [Cint 1],
outL "ok" [Cint 15],
inpL "water" [Cint 1],
outL "ok" [Cint 16],
outL "coffee" [],
GateValue δ [],
GateValue δ []
]
let checkExample = go 0 0 exampleObserved
assertEqual ("expected conformal trace like " <> show exampleObserved <> ", got " <> show observed) checkObserved checkExample
assertEqual "expected pass " Pass verdict
where
inpL g vals = GateValue (In (InputAttempt(g, True))) vals
outL g vals = GateValue (Out (OutSusp g)) vals
go ds waterlevel [] = (ds, waterlevel)
go ds waterlevel (GateValue (Out Quiescence) []:os) = go (ds+1) waterlevel os
go ds waterlevel gv@(GateValue x y:os)
| x == In (InputAttempt ("water", True))
, [Cint w] <- y = go ds (waterlevel+w) os
| x == Out (OutSusp "ok")
, [Cint w] <- y
, w == waterlevel = go ds waterlevel os
| x == Out (OutSusp "coffee")
, [] <- y
, waterlevel > 15 = go ds waterlevel os
| otherwise = error $ "wrong gatevalue: " <> show gv
pvarf :: Variable
pvarf = (Variable "p" FloatType)
xvarf :: Variable
xvarf = (Variable "x" FloatType)
stsExampleInitAssignFloat :: Valuation
stsExampleInitAssignFloat = fromConstantsMap $ Map.singleton xvarf (Cfloat (0.0 :: Double))
stsExampleFloat :: IOSTS FreeLattice Integer String String
stsExampleFloat =
let p = sVar pvarf :: Expr Double
x = sVar xvarf :: Expr Double
water = SymInteract (In "water") [pvarf]
ok = SymInteract (Out "ok") [pvarf]
coffee = SymInteract (Out "coffee") []
waterGuard = 1 .<= p .&& p .<= 10
waterAssign = assignment [xvarf =: x .+ p]
okGuard = x .== p
coffeeGuard = x .>= sConst (14.5 :: Double)
initConf = disjunction [0] :: FreeLattice Integer
switches = \case
0 -> Map.fromList [(water, disjunction [(stsTLoc waterGuard waterAssign, 1)]),
(coffee, disjunction [(stsTLoc coffeeGuard noAssignment, 2)])]
1 -> Map.fromList [(ok, disjunction [(stsTLoc okGuard noAssignment, 0)])]
2 -> Map.empty
in automaton initConf (Set.fromList [water,ok,coffee]) switches
stsExampleIntrprFloat :: STSIntrp FreeLattice Integer (IOAct String String)
stsExampleIntrprFloat = interpretSTS stsExampleFloat stsExampleInitAssignFloat
getSTSIntrpStateFloat :: Integer -> Double -> FreeLattice (IntrpState Integer)
getSTSIntrpStateFloat loc val = disjunction [IntrpState loc $ fromConstantsMap $ Map.singleton (Variable "x" FloatType) (Cfloat val)]
testSTSHappyFlowFloat :: Test
testSTSHappyFlowFloat = TestCase $ do
-- assertEqual "\ninitial state " (getSTSIntrpStateFloat 0 0.0) (stateConf stsExampleIntrpr)
let intrp2 = after stsExampleIntrprFloat (GateValue (In "water") [Cfloat (7.5 :: Double)])
assertEqual "after water 7.5: " (getSTSIntrpStateFloat 1 (7.5 :: Double)) (stateConf intrp2)
-- let intrp3 = after intrp2 (GateValue (Out "ok") [Cfloat 7.5])
-- assertEqual "after ok 7.5: " (getSTSIntrpStateFloat 0 (7.5 :: Double)) (stateConf intrp3)
-- let intrp4 = after intrp3 (GateValue (In "water") [Cfloat 8.5])
-- assertEqual "after water 8.5: " (getSTSIntrpStateFloat 1 (16.0 :: Double)) (stateConf intrp4)
-- let intrp5 = after intrp4 (GateValue (Out "ok") [Cfloat 16.0])
-- assertEqual "after ok 16.0: " (getSTSIntrpStateFloat 0 (16.0 :: Double)) (stateConf intrp5)
-- let intrp6 = after intrp5 (GateValue (Out "coffee") [])
-- assertEqual "after coffee: " (getSTSIntrpStateFloat 2 (16.0 :: Double)) (stateConf intrp6)
return()
stsExample2 :: (IOSTS FreeLattice Integer String String, IOSTS FreeLattice Integer String String)
stsExample2 =
let p = sVar pvar :: Expr Integer
x = sVar xvar :: Expr Integer
water = SymInteract (In "water") [pvar]
ok = SymInteract (Out "ok") [pvar]
coffee = SymInteract (Out "coffee") []
waterGuard = 1 .<= p .&& p .<= 4
waterGuard1 = 4 .<= p .&& p .<= 10
waterAssign = assignment [xvar =: x .+ p]
okGuard = x .== p
coffeeGuard = x .>= 15
initConf = atom 0
switches = \q -> case q of
0 -> Map.fromList [(water, atom (stsTLoc waterGuard waterAssign, 1) /\ atom (stsTLoc waterGuard1 waterAssign, 2) )]
1 -> Map.fromList [(ok, atom (stsTLoc okGuard noAssignment, 0))]
2 -> Map.fromList [(ok, atom (stsTLoc okGuard noAssignment, 0))]
initConf2 = atom 0 /\ atom 2
switches2 = \q -> case q of
0 -> Map.fromList [(water, atom (stsTLoc waterGuard waterAssign, 1))]
1 -> Map.fromList [(ok, atom (stsTLoc okGuard noAssignment, 0))]
2 -> Map.fromList [(water, atom (stsTLoc waterGuard1 waterAssign, 3))]
3 -> Map.fromList [(ok, atom (stsTLoc okGuard noAssignment, 2))]
in (automaton initConf (Set.fromList [water,ok,coffee]) switches, automaton initConf2 (Set.fromList [water,ok,coffee]) switches2)
stsExampleIntrpr2a :: STSIntrp FreeLattice Integer (IOAct String String)
stsExampleIntrpr2a = interpretSTS (fst stsExample2) stsExampleInitAssign
stsExampleIntrpr2b :: STSIntrp FreeLattice Integer (IOAct String String)
stsExampleIntrpr2b = interpretSTS (snd stsExample2) stsExampleInitAssign
getSTSValuation :: Integer -> Valuation
getSTSValuation val = fromConstantsMap $ Map.singleton (Variable "x" IntType) (Cint val)
getSTSIntrpState2 :: Integer -> Integer -> FreeLattice (IntrpState Integer)
getSTSIntrpState2 loc val = atom (IntrpState loc $ getSTSValuation val)
testLatticeCoffeeSTS :: Test
testLatticeCoffeeSTS = TestCase $ do
assertEqual "\ninitial state " (getSTSIntrpState2 0 0) (stateConf stsExampleIntrpr2a)
assertEqual "\ninitial state " (getSTSIntrpState2 0 0 /\ getSTSIntrpState2 2 0) (stateConf stsExampleIntrpr2b)
let intrp2a = after stsExampleIntrpr2a (GateValue (In "water") [Cint 3])
assertEqual "2a after water 3: " (getSTSIntrpState2 1 3) (stateConf intrp2a)
let intrp2b = after stsExampleIntrpr2b (GateValue (In "water") [Cint 3])
assertEqual "2b after water 3: " (getSTSIntrpState2 1 3) (stateConf intrp2b)
let intrp3a = after intrp2a (GateValue (Out "ok") [Cint 3])
assertEqual "2a after ok 3: " (getSTSIntrpState2 0 3) (stateConf intrp3a)
let intrp3b = after intrp2b (GateValue (Out "ok") [Cint 3])
assertEqual "2b after ok 3: " (getSTSIntrpState2 0 3) (stateConf intrp3b)
let intrp4a = after intrp3a (GateValue (In "water") [Cint 4])
assertEqual "2a after water 4: " (getSTSIntrpState2 1 7 /\ getSTSIntrpState2 2 7) (stateConf intrp4a)
let intrp4b = after intrp3b (GateValue (In "water") [Cint 4])
assertEqual "2b after water 4: " (getSTSIntrpState2 1 7) (stateConf intrp4b)
let intrp5a = after intrp4a (GateValue (Out "ok") [Cint 7])
assertEqual "2a after ok 7: " (getSTSIntrpState2 0 7) (stateConf intrp5a)
let intrp5b = after intrp4b (GateValue (Out "ok") [Cint 7])
assertEqual "2b after ok 7: " (getSTSIntrpState2 0 7) (stateConf intrp5b)
let intrp6a = after intrp5a (GateValue (In "water") [Cint 5])
assertEqual "2a after water 5: " (getSTSIntrpState2 2 12) (stateConf intrp6a)
let intrp6b = after intrp5b (GateValue (In "water") [Cint 5])
assertEqual "2b after water 5: " underspecified (stateConf intrp6b)
{- specification:
end(p,q)
〚p+q=x+2〛
╱——————>•————\
x:=0 ╱ \
———>•—————————>• end(p,q) ———>•
start(p) ╲ 〚p-q=x〛 /!done
〚1<p<3〛 ╲——————>•————/
x ≔ p
parameterized by
* whether start and end gates are input or output
* the type of branching from the second state (conjunction or disjunction)
* whether to split the second state into two, where the branching occurs on the first transition (with equal guards) instead of the second
-}
specParameterized :: (String -> IOAct String String) -> (String -> IOAct String String) -> (forall a.FreeLatticeSlow a -> FreeLatticeSlow a -> FreeLatticeSlow a) -> Bool -> IOSTS FreeLatticeSlow Integer String String
specParameterized startType endType comp splitFirst =
let p = sVar pvar :: Expr Integer
q = sVar qvar :: Expr Integer
x = sVar xvar :: Expr Integer
start = SymInteract (startType "start") [pvar]
end = SymInteract (endType "end") [pvar, qvar]
done = SymInteract (Out "done") []
initConf = pure 0 :: FreeLatticeSlow Integer
guardStart = 1 .< p .&& p .< 3
guardEnd1 = p .+ q .== x .+ 2
guardEnd2 = p .- q .== x
assignX = assignment [xvar =: p]
switches =
if splitFirst
then \s -> case s of
0 -> Map.fromList [(start, pure (stsTLoc guardStart assignX, 1) `comp` pure (stsTLoc guardStart assignX, 2))]
1 -> Map.fromList [(end, pure (stsTLoc guardEnd1 noAssignment, 3))]
2 -> Map.fromList [(end, pure (stsTLoc guardEnd2 noAssignment, 4))]
3 -> Map.fromList [(done, pure (stsTLoc sTrue noAssignment, 5))]
4 -> Map.fromList [(done, pure (stsTLoc sTrue noAssignment, 5))]
5 -> Map.empty
else \s -> case s of
0 -> Map.fromList [(start, pure (stsTLoc guardStart assignX, 1))]
1 -> Map.fromList [(end, pure (stsTLoc guardEnd1 noAssignment, 2) `comp` pure (stsTLoc guardEnd2 noAssignment, 3))]
2 -> Map.fromList [(done, pure (stsTLoc sTrue noAssignment, 4))]
3 -> Map.fromList [(done, pure (stsTLoc sTrue noAssignment, 4))]
4 -> Map.empty
in automaton initConf (Set.fromList [start, end, done]) switches
{- implementation:
start(p) end(p,q) !done
———>•—————————>•—————————>•—————————>•
parameterized by
* whether start and end gates are input or output
* p and q (note, this means that only s specific, single concrete transition start(p) and single concrete transition end(p,q) is defined)
-}
t1 :: (Ord i, Ord o, Num a1, Num a2, IsString t1, IsString t2, IsString o, Eq a1) => (t1 -> IOAct i o) -> (t2 -> IOAct i o) -> Integer -> Integer -> Integer -> a1 -> Map.Map (GateValue (IOAct i o)) a2
t1 startType _ p1 _ _ 0 = Map.fromList $ [((GateValue (startType "start") [Cint p1]), 1)]
t1 _ endType _ p2 q2 1 = Map.fromList $ [((GateValue (endType "end") [Cint p2, Cint q2]), 2)]
t1 _ _ _ _ _ 2 = Map.fromList $ [((GateValue (Out "done") []), 3)]
t1 _ _ _ _ _ 3 = Map.fromList $ []
impParameterized :: (String -> IOAct String String) -> (String -> IOAct String String) -> Integer -> Integer -> Integer -> IO (Adapter.Adapter (SuspendedIFGateValue String String) (Maybe (GateValue String)))
impParameterized startType endType p1 p2 q2 = do
imp <- pureAdapter (mkStdGen 123) 0.5 (Map.mapKeys gateValueAsIOAct <$> t1 startType endType p1 p2 q2) (0 :: Integer) :: IO (Adapter.Adapter (SuspendedIF (GateValue String) (GateValue String)) (Maybe (GateValue String)))
Adapter.mapActionsFromSut toIOGateValue imp
testLatticeSTSParameterized' :: String -> Bool -> (forall a. FreeLatticeSlow a -> FreeLatticeSlow a -> FreeLatticeSlow a) -> Bool -> Integer -> Integer -> Integer -> Maybe [SuspendedIFGateValue String String] -> Test
testLatticeSTSParameterized' testName inputThenOut comp splitFirst p1 p2 q2 expectedNonConformalTrace = TestCase $ do
let (startType, endType, startType', endType') =
if inputThenOut
then (In, Out, inp, out)
else (Out, In, out, inp)
let nrSteps = 4
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.0 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impParameterized startType endType p1 p2 q2
let specIntrpr = interpretSTSQuiescentInputAttemptConcrete (specParameterized startType endType comp splitFirst) stsExampleInitAssign
(verdict, ((observed, _), _)) <- runSMTTester specIntrpr testSelector imp
case expectedNonConformalTrace of
Nothing -> do
assertEqual (testName ++ ": expected Pass after " ++ show observed) Pass verdict
assertEqual (testName ++ ": expected conformal trace") [
startType' "start" [Cint p1],
endType' "end" [Cint p2, Cint q2],
out "done" [],
GateValue δ []
] observed
Just t -> do
assertEqual (testName ++ ": expected Fail after " ++ show observed) Fail verdict
assertEqual (testName ++ ": expected nonconformal trace") t observed
inp :: i -> [Constant] -> GateValue (IOAct (InputAttempt i) o)
inp g vals = GateValue (In (InputAttempt(g, True))) vals
inpf :: i -> [Constant] -> GateValue (IOAct (InputAttempt i) o)
inpf g vals = GateValue (In (InputAttempt(g, False))) vals
out :: o -> [Constant] -> GateValue (IOAct i (Suspended o))
out g vals = GateValue (Out (OutSusp g)) vals
testLatticeSTSParameterized :: String -> Bool -> (forall a. FreeLatticeSlow a -> FreeLatticeSlow a -> FreeLatticeSlow a) -> Integer -> Integer -> Integer -> Maybe [SuspendedIFGateValue String String] -> [Test]
testLatticeSTSParameterized testName inputThenOut comp p1 p2 q2 expectedNonConformalTrace = [
testLatticeSTSParameterized' testName inputThenOut comp False p1 p2 q2 expectedNonConformalTrace,
testLatticeSTSParameterized' (testName ++ "'") inputThenOut comp True p1 p2 q2 expectedNonConformalTrace
]
testLatticeSTS :: [Test]
testLatticeSTS = concat [
-- TODO add some cases for quiescence, immediate wrong input failure values, etc.
testLatticeSTSParameterized "a1" inputThenOutput (\/) 2 2 2 Nothing, -- pass: output (2,2) satisfies the first guard
testLatticeSTSParameterized "a2" inputThenOutput (\/) 2 4 2 Nothing, -- pass: output (4,2) satisfies the second guard
testLatticeSTSParameterized "a3" inputThenOutput (\/) 2 3 1 Nothing, -- pass: output (3,1) satisfies both guards
testLatticeSTSParameterized "a4" inputThenOutput (\/) 2 4 4 (Just [inp "start" [Cint 2], out "end" [Cint 4, Cint 4]]), -- fail: output (4,4) satisfies neither guard
testLatticeSTSParameterized "a5" inputThenOutput (/\) 2 2 2 (Just [inp "start" [Cint 2], out "end" [Cint 2, Cint 2]]), -- fail: output (2,2) satisfies the first guards, but not both
testLatticeSTSParameterized "a6" inputThenOutput (/\) 2 4 2 (Just [inp "start" [Cint 2], out "end" [Cint 4, Cint 2]]), -- fail: output (4,2) satisfies the second guards, but not both
testLatticeSTSParameterized "a7" inputThenOutput (/\) 2 4 4 (Just [inp "start" [Cint 2], out "end" [Cint 4, Cint 4]]), -- fail: output (4,4) satisfies neither guard
testLatticeSTSParameterized "a8" inputThenOutput (/\) 2 3 1 Nothing, -- pass: output (3,1) satisfies both guards
testLatticeSTSParameterized "b1" outputThenInput (\/) 2 3 1 Nothing, -- pass: (3,1) is the only input that matches both guards, so is the only specified input overall, thus will be tested and observed
testLatticeSTSParameterized "b2" outputThenInput (\/) 2 5 5 (Just [out "start" [Cint 2], inpf "end" [Cint 3, Cint 1]]) -- pass: (3,1) is the only input that matches both guards, so is the only specified input overall, thus will be tested but refused
-- FIXME the next tests are actually unsound: it will pass under the assumption that the test selection (SMT solver) will pick the last two number parameters as input,
-- but if not, the test case will incorrectly fail. To fix this, change the implementation to accept any (p,q) satisfying any of the guards 〚p+q=4〛 or 〚p-q=2〛
--testLatticeSTSParameterized "b3" outputThenInput (/\) 2 0 (-2) Nothing, -- pass: (0,-2) is an input that matches one of the guards, so is specified, thus may be tested and in that case will be observed
--testLatticeSTSParameterized "b4" outputThenInput (/\) 2 5 5 (Just [out "start" [Cint 2], inpf "end" [Cint 0, Cint (-2)]]) -- fail: the tester will pick an input that matches one of the guards, but will be rejected by the implementation
]
where
inputThenOutput = True
outputThenInput = False
{- specification:
x:=0
———>•—————————>•———————————>•
?start(p) !end(p,q)
〚1<p<3〛 〚p+q=p+q+x〛
x ≔ p
note, the guard of the second transition is not satisfiable so the second state is quiescent
-}
specQ :: IOSTS FreeLatticeSlow Integer String String
specQ =
let p = sVar pvar :: Expr Integer
q = sVar qvar :: Expr Integer
x = sVar xvar :: Expr Integer
start = SymInteract (In "start") [pvar]
end = SymInteract (Out "end") [pvar, qvar]
initConf = pure 0 :: FreeLatticeSlow Integer
guardStart = 1 .< p .&& p .< 3
guardEnd = p .+ q .== p .+ q .+ x
assignX = assignment [xvar =: p]
switches = \s -> case s of
0 -> Map.fromList [(start, pure (stsTLoc guardStart assignX, 1))]
1 -> Map.fromList [(end, pure (stsTLoc guardEnd noAssignment, 2))]
2 -> Map.empty
in automaton initConf (Set.fromList [start, end]) switches
{- implementation:
start(p)
———>•—————————>•
parameterized by
* whether start gate is input or output
* p
-}
tq :: (Ord g, IsString t, Num a1, Num a2, Eq a1) => (t -> g) -> Integer -> a1 -> Map.Map (GateValue g) a2
tq startType p 0 = Map.fromList $ [((GateValue (startType "start") [Cint p]), 1)]
tq _ _ 1 = Map.fromList $ []
impQParameterized :: (String -> IOAct String String) -> Integer -> IO (Adapter.Adapter (SuspendedIFGateValue String String) (Maybe (GateValue String)))
impQParameterized startType p = do
imp <- pureAdapter (mkStdGen 123) 0.5 (Map.mapKeys gateValueAsIOAct <$> tq startType p) (0 :: Integer) :: IO (Adapter.Adapter (SuspendedIF (GateValue String) (GateValue String)) (Maybe (GateValue String)))
Adapter.mapActionsFromSut toIOGateValue imp
testLatticeSTSQuiescentPass :: String -> Bool -> Test
testLatticeSTSQuiescentPass testName _ = TestCase $ do
let nrSteps = 2
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.0 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impQParameterized In 2
let specIntrpr = interpretSTSQuiescentInputAttemptConcrete specQ stsExampleInitAssign
(verdict, ((observed, _), _)) <- runSMTTester specIntrpr testSelector imp
assertEqual (testName ++ ": expected Pass after " ++ show observed) Pass verdict
assertEqual (testName ++ ": expected conformal trace") [
inp "start" [Cint 2],
GateValue δ []
] observed
testLatticeSTSQuiescentFail1 :: String -> Bool -> Test
testLatticeSTSQuiescentFail1 testName splitFirst = TestCase $ do
let nrSteps = 2
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.0 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impQParameterized In 2
let specIntrpr = interpretSTSQuiescentInputAttemptConcrete (specParameterized In Out (\/) splitFirst) stsExampleInitAssign
(verdict, ((observed, _), _)) <- runSMTTester specIntrpr testSelector imp
assertEqual (testName ++ ": expected Pass after " ++ show observed) Fail verdict
assertEqual (testName ++ ": expected nonconformal trace") [
inp "start" [Cint 2],
GateValue δ []
] observed
testLatticeSTSQuiescentFail2 :: String -> Bool -> Test
testLatticeSTSQuiescentFail2 testName _ = TestCase $ do
let nrSteps = 2
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.0 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impParameterized In Out 2 42 42
let specIntrpr = interpretSTSQuiescentInputAttemptConcrete specQ stsExampleInitAssign
(verdict, ((observed, _), _)) <- runSMTTester specIntrpr testSelector imp
assertEqual (testName ++ ": expected Pass after " ++ show observed) Fail verdict
assertEqual (testName ++ ": expected nonconformal trace") [
inp "start" [Cint 2],
out "end" [Cint 42, Cint 42]
] observed
{- specification:
!end(p,q)
〚p+q=x+2〛
╱——————————\
x:=0 ╱ \
———>•—————————>• ) !end(p,q) ———>•
?start(p) ╲ 〚p+q=x〛 /
〚1<p<3〛 ╲——————————/
x ≔ p
parameterized by whether to split the second state into two, where the branching occurs on the first transition (with equal guards) instead of the second
-}
specUnimplementableParameterized :: Bool -> IOSTS FreeLatticeSlow Integer String String
specUnimplementableParameterized splitFirst =
let p = sVar pvar :: Expr Integer
q = sVar qvar :: Expr Integer
x = sVar xvar :: Expr Integer
start = SymInteract (In "start") [pvar]
end = SymInteract (Out "end") [pvar, qvar]
initConf = pure 0 :: FreeLatticeSlow Integer
guardStart = 1 .< p .&& p .< 3
guardEnd1 = p .+ q .== x .+ 2
guardEnd2 = p .+ q .== x
assignX = assignment [xvar =: p]
switches =
if splitFirst
then \s -> case s of
0 -> Map.fromList [(start, pure (stsTLoc guardStart assignX, 1) /\ pure (stsTLoc guardStart assignX, 2))]
1 -> Map.fromList [(end, pure (stsTLoc guardEnd1 noAssignment, 3))]
2 -> Map.fromList [(end, pure (stsTLoc guardEnd2 noAssignment, 3))]
3 -> Map.empty
else \s -> case s of
0 -> Map.fromList [(start, pure (stsTLoc guardStart assignX, 1))]
1 -> Map.fromList [(end, pure (stsTLoc guardEnd1 noAssignment, 2) /\ pure (stsTLoc guardEnd2 noAssignment, 3))]
2 -> Map.empty
3 -> Map.empty
in automaton initConf (Set.fromList [start, end]) switches
testLatticeSTSUnimplementable :: String -> Bool -> Test
testLatticeSTSUnimplementable testName splitFirst = TestCase $ do
let nrSteps = 2
let testSelector = randomDataOrWaitForOutputTestSelectorFromSeed 456 0.0 `untilCondition` stopAfterSteps nrSteps
`observingOnly` traceObserver `andObserving` stateObserver `andObserving` inconclusiveStateObserver
imp <- impQParameterized In 2
let specIntrpr = interpretSTSQuiescentInputAttemptConcrete (specUnimplementableParameterized splitFirst) stsExampleInitAssign
(verdict, ((observed, _), _)) <- runSMTTester specIntrpr testSelector imp
assertEqual (testName ++ ": expected Fail after " ++ show observed) Fail verdict
assertEqual (testName ++ ": expected nonconformal trace") [
inp "start" [Cint 2],
GateValue δ []
] observed
testLatticeSTSQuiescence :: [Test]
testLatticeSTSQuiescence = [
testLatticeSTSQuiescentPass "q1" True, -- a quiescent implementation and STS will lead to a pass
testLatticeSTSQuiescentPass "q2'" False, -- a quiescent implementation and STS will lead to a pass
testLatticeSTSQuiescentFail1 "q3" True, -- a quiescent implementation will fail against a non-quiescent specification
testLatticeSTSQuiescentFail1 "q4" False, -- a quiescent implementation will fail against a non-quiescent specification
testLatticeSTSQuiescentFail2 "q3" True, -- a non-quiescent implementation will fail against a quiescent specification
testLatticeSTSQuiescentFail2 "q4" False, -- a non-quiescent implementation will fail against a quiescent specification
testLatticeSTSUnimplementable "u1" True, -- an unimplementable specification (two conjunctive conditions contradicting eachother) is not implemented by a quiescent implementation
testLatticeSTSUnimplementable "u2'" False -- an unimplementable specification (two conjunctive conditions contradicting eachother) is not implemented by a quiescent implementation
]