Tests: fix

src/API.hs

@@ -71,15 +71,15 @@ compareSpec m pMode methodA methodB = do
 
             mv1 <- newEmptyMVar
             mv2 <- if m == Debug then newEmptyMVar else return mv1
-            mapM_ (compareSpecHelper mv1) [ ("Z3", Z3.equivalentTo)
-                                          , ("Test", Test.equivalentTo)
-                                          ]
+            mapM_ compareSpecHelper [ (mv1, "Z3", Z3.equivalentTo)
+                                    , (mv2, "Test", Test.equivalentTo)
+                                    ]
             res1 <- readMVar mv1
             res2 <- readMVar mv2 -- if Release, this won't block
             return $ getRes m res1 res2
             where -- | Runs f on a separate thread and stores the result in mv.
-                  compareSpecHelper mv (name, impl) = forkIO $ do
-                    res <- checkSpec name impl (preL, preL') (postL, postL')
+            compareSpecHelper (mv, name, impl) = forkIO $ do
+                    res <- checkSpec name impl (preL, preL') (postL, postL') 
                     res `seq` putMVar mv res
 
 -- | Makes sure that both Responses are the same, otherwise, if we

src/LogicIR/Backend/QuickCheck/API.hs

 module LogicIR.Backend.QuickCheck.API (equivalentTo) where
 
-import Control.Arrow (second)
+import Control.Arrow ((***))
 import Data.Map (Map)
 import qualified Data.Map.Lazy as M
 import Data.Maybe (fromJust, fromMaybe, isNothing)
@@ -16,17 +16,13 @@ equivalentTo lexpr lexpr' = do
     (eq, testModel) <- testEquality 1000 lexpr lexpr'
     if eq
     then return Equivalent
-    else return $ NotEquivalent $ toModel testModel
+    else return $ NotEquivalent $ toZ3Model testModel
 
-toModel :: (QC.Model, QC.ArrayModel) -> Model
-toModel (m, arrayM) = do
-    let arrayKeys = map LVar $ M.keys arrayM
-    let arrayVals = map (map LConst) $ M.elems arrayM
-    let arrayKVs = zip arrayKeys (map toModelVals arrayVals)
-    let modelKVs = map (second toModelVal) m
-    let model = arrayKVs ++ modelKVs
-    M.fromList $ map makePretty model
-    where makePretty (k,v) = (prettyLExpr k, v)
+toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
+toZ3Model (m, arrayM) =
+    M.fromList $
+      map (prettyLExpr *** toModelVal) m ++
+      map ((prettyLExpr *** toModelVals) . (LVar *** fmap LConst)) (M.toList arrayM)
 
 toModelVal :: LExpr -> ModelVal
 toModelVal (LConst (CBool b)) = BoolVal b
@@ -34,4 +30,4 @@ toModelVal (LConst (CInt  i)) = IntVal  $ toInteger i
 toModelVal (LConst (CReal r)) = RealVal r
 
 toModelVals :: [LExpr] -> ModelVal
-toModelVals es@(x:xs) = ManyVal $ map toModelVal es
+toModelVals = ManyVal . map toModelVal

test/TEquivalenceClasses.hs

@@ -14,11 +14,11 @@ import Javawlp.Engine.HelperFunctions (parseMethodIds)
 import Model
 
 testEquiv :: Response -> String -> String -> String -> Assertion
-testEquiv b src s s' =
-  (case unsafePerformIO (hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')) of
+testEquiv b src s s' = do
+  res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
+  (case res of
     NotEquivalent x -> NotEquivalent emptyModel
-    x               -> x
-   ) @?= b
+    x               -> x) @?= b
 (.==) = testEquiv Equivalent
 (.!=) = testEquiv $ NotEquivalent emptyModel
 

test/TExamples.hs

@@ -10,11 +10,11 @@ import Model
 src = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 
 testEquiv :: Response -> String -> String -> Assertion
-testEquiv b s s' =
-  (case unsafePerformIO (hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')) of
+testEquiv b s s' = do
+  res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
+  (case res of
     NotEquivalent _ -> NotEquivalent emptyModel
-    x               -> x
-   ) @?= b
+    x               -> x) @?= b
 (.==) = testEquiv Equivalent
 (.!=) = testEquiv $ NotEquivalent emptyModel
 (.??) = testEquiv Timeout