Added feedback to test module and debug mode option to command line. Fixed bug...

Added feedback to test module and debug mode option to command line. Fixed bug in the way Z3/Test concurrency was handled. Small changes/fixes in readme. Added more comments.

README.md

@@ -22,7 +22,7 @@ Command-line usage:
 ```
 stack exec javawlp --
   [--srcA STRING] [--srcB STRING] [-a STRING] [-b STRING]
-  [-w|--runServer] [-p|--port INT]
+  [-w|--runServer] [-p|--port INT] [-d|--debugMode]
 ```
 
 To run a comparison between two methods:
@@ -31,6 +31,7 @@ To run a comparison between two methods:
   --srcA 'examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java' -a 'real1' \
   --srcB 'examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java' -b 'real2'
 ```
+The command shown above will compare the "real1" method from Main.java with the "real2" method from Main.java using both an SMT solver (Z3) and a brute-force testing approach concurrently. The result from whoever finishes first will be returned. To see the results from both the Z3 and testing approach, use the `-d` flag to run in debug mode.
 
 To run the server API at port 8080:
 ```
@@ -44,7 +45,7 @@ To query the server (see  for available options):
 
 To get the API docs from the server:
 - Markdown: Visit `<server_url>:8080/docs`
-- Swagger: Visit ``<server_url>:8080/api-swagger`
+- Swagger: Visit `<server_url>:8080/api-swagger`
 - [API.md](https://git.science.uu.nl/impresshs/javawlp/blob/master/API.md)
 
 To run the tests:

app/Main.hs

@@ -15,6 +15,7 @@ data Options = Options
   , methodB   :: String
   , runServer :: Bool
   , port      :: Int
+  , mode      :: Mode
   }
 
 -- | Parsing of command-line options.
@@ -59,6 +60,15 @@ parseOptions = Options
       <> value 8888
       <> help "Listening port"
       )
+  <*> (toMode <$> switch
+      (  short 'd'
+      <> long  "debugMode"
+      <> help "Run in debug mode (instead of release)"
+      ))
+
+toMode :: Bool -> Mode
+toMode False = Release
+toMode True  = Debug
 
 withInfo :: Parser a -> String -> ParserInfo a
 withInfo opts desc = info (helper <*> opts) $ progDesc desc
@@ -69,10 +79,10 @@ main = runMain =<< execParser (parseOptions `withInfo` "Java WLP")
 
 -- | Run.
 runMain :: Options -> IO ()
-runMain (Options srcA srcB methA methB serverFlag portNo) =
+runMain (Options srcA srcB methA methB serverFlag portNo runMode) =
   if serverFlag then
     runApi portNo
   else do
     when (methA == "_default_") $ fail "No files given."
-    response <- compareSpec Release File (srcA, methA) (srcB, methB)
+    response <- compareSpec runMode File (srcA, methA) (srcB, methB)
     print response

src/API.hs

@@ -7,6 +7,7 @@ import Data.List.Split    (splitOn)
 import Data.Maybe
 import Prelude            hiding (log)
 import System.IO
+import System.Timeout
 
 import Javawlp.Engine.HelperFunctions
 import Javawlp.Engine.Types
@@ -70,19 +71,53 @@ compareSpec m pMode methodA methodB = do
           log $ "LExprA:\n" ++ prettyLExpr postL ++ "\n"
           log $ "LExprB:\n" ++ prettyLExpr postL' ++ "\n"
 
+          -- Run Z3 with mv1 and Test with mv2. If Release, they both get the same
+          -- mvar and whoever finishes first will therefore write to both
+          -- mv1 and mv2. If Debug, they both get a different MVar, we wait for
+          -- both and then compare their results.
           mv1 <- newEmptyMVar
           mv2 <- if m == Debug then newEmptyMVar else return mv1
-          mapM_ compareSpecHelper [ (mv1, "Z3", Z3.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
+          waitForResult m mv1 mv2
           where -- | Runs f on a separate thread and stores the result in mv.
+                compareSpecHelper :: (MVar Response, String, EquivImpl) -> IO ThreadId
                 compareSpecHelper (mv, name, impl) = forkIO $ do
                   resp <- checkEquiv name impl (preL, preL') (postL, postL')
                   resp `seq` putMVar mv resp
 
+-- Waits (blocking) until it has a Response to return.
+waitForResult :: Mode -> MVar Response -> MVar Response -> IO Response
+waitForResult Debug   = waitForResultDebug
+waitForResult Release = waitForResultRelease
+
+-- | Run both `Z3` and `Test`, wait for their responses (no matter how slow they
+--   are) and compare them.
+waitForResultDebug :: MVar Response -> MVar Response -> IO Response
+waitForResultDebug z3mv testmv = do
+  z3res   <- readMVar z3mv
+  testres <- readMVar testmv
+  return $ getRes Debug z3res testres
+
+-- | Try to compare using Z3 first. If timeout is reached, fall back on Test. If
+--   test is too slow as well, give up.
+waitForResultRelease :: MVar Response -> MVar Response -> IO Response
+waitForResultRelease z3mv testmv = do
+      let t      = fromIntegral (Z3.timeoutTime * 1000) -- one second in microseconds
+      maybeZ3Res <- timeout t (readMVar z3mv)
+      -- Z3 is too slow.
+      if maybeZ3Res == Nothing then do
+          maybeTestRes <- timeout t (readMVar testmv)
+          -- Test is too slow as well.
+          if maybeTestRes == Nothing then
+            return Timeout
+          else
+            return $ fromJust maybeTestRes
+      -- Z3 was fast enough
+      else
+        return $ fromJust maybeZ3Res
+
 -- | Makes sure that both Responses are the same, otherwise, if we
 --   run in debug mode, an error will be thrown. If not in debug mode,
 --   the first given Response (that of the theorem prover) will be

src/LogicIR/Backend/QuickCheck/API.hs

@@ -4,20 +4,24 @@ import           Control.Arrow                             ((***))
 import qualified Data.Map.Lazy                             as M
 import qualified LogicIR.Backend.QuickCheck.ModelGenerator as QC
 import           LogicIR.Backend.QuickCheck.Test
-import           LogicIR.Expr                              hiding (b, r)
+import           LogicIR.Expr                              hiding (b,r,n)
 import           LogicIR.Pretty                            (prettyLExpr)
 import           Model
 
 -- | Determine the equality of two method's pre/post conditions.
-equivalentTo :: LExpr -> LExpr -> IO Response
+equivalentTo :: LExprTeacher -> LExprStudent -> IO Response
 equivalentTo lexpr lexpr' = do
-    (eq, testModel) <- testEquality 1000 lexpr lexpr'
-    let feedback = Feedback { pre = defFeedback -- TODO check which combinations are possible
-                            , post = defFeedback -- leave as is
-                            }
-    if eq
-    then return Equivalent
-    else return $ NotEquivalent (toZ3Model testModel) feedback
+    (feedbackCount, counterModel) <- testEquality 500 lexpr lexpr'
+    if equal feedbackCount then
+      return Equivalent
+    else do
+      let fb = toSingleFeedback feedbackCount
+      let feedback = Feedback { pre = fb, post = defFeedback }
+      return $ NotEquivalent (toZ3Model counterModel) feedback
+
+toSingleFeedback :: FeedbackCount -> SingleFeedback
+toSingleFeedback (a,b,c,d) = (n a, n b, n c, n d)
+  where n = (0<)
 
 toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
 toZ3Model (m, arrayM) =

src/LogicIR/Backend/QuickCheck/Test.hs

-module LogicIR.Backend.QuickCheck.Test (testEquality) where
+module LogicIR.Backend.QuickCheck.Test ( testEquality
+                                       , LExprTeacher
+                                       , LExprStudent
+                                       , FeedbackCount
+                                       , equal
+                                       ) where
 
 import LogicIR.Expr
 import LogicIR.Fold
@@ -8,25 +13,59 @@ import Data.Maybe (fromMaybe, isNothing, fromJust)
 import Data.List (find, (\\))
 import qualified Data.Map.Lazy as M
 
-test :: LExpr -> LExpr -> IO (Bool, Model, ArrayModel)
-test e1 e2 = do
-    (res1,(m,arrM,_)) <- testLExpr e1
-    evalInfo'         <- expandEvalInfo e2 (m, arrM)
-    res2              <- testModel e2 evalInfo'
-    let (primitivesModel, arrayModel, _) = evalInfo'
-    return (res1 == res2, primitivesModel, arrayModel)
+type LExprTeacher = LExpr
+type LExprStudent = LExpr
+
+-- | Contains how often any type of feedback occured over x runs (where x is
+--   obviously the sum of the four integers). Order of Integers in tuple
+--   is the same as in Model.SingleFeedback
+type FeedbackCount = ( Int -- T-T
+                     , Int -- T-F
+                     , Int -- F-T
+                     , Int -- F-F
+                     )
+
+defFbCount :: FeedbackCount
+defFbCount = (0,0,0,0)
+
+add :: FeedbackCount -> FeedbackCount -> FeedbackCount
+add (w,x,y,z) (w',x',y',z') = (w+w',x+x',y+y',z+z')
+
+-- | Converts two Bools to FeedbackCount. First Bool is the Bool you get when
+--   the TeacherLExpr was evaluated using some Model+ArrayModel m, the second
+--   one the bool you get when you evaluate te StudentLExpr using m.
+toFeedbackCount :: Bool -> Bool -> FeedbackCount
+toFeedbackCount True  True  = (1,0,0,0)
+toFeedbackCount True  False = (0,1,0,0)
+toFeedbackCount False True  = (0,0,1,0)
+toFeedbackCount False False = (0,0,0,1)
+
+-- | Returns True if, on we have 0 TF or FT occurences (in other words: occurences
+--   where the teacher and student specification gave a different result)
+equal :: FeedbackCount -> Bool
+equal (_,tf,ft,_) = tf == 0 && ft == 0
 
 -- Calls 'test' multiple times.
-testEquality :: Int -> LExpr -> LExpr -> IO (Bool, (Model, ArrayModel))
-testEquality 0 _ _ =
-    return (True, ([], M.empty))
+testEquality :: Int -> LExprTeacher -> LExprStudent -> IO (FeedbackCount, (Model, ArrayModel))
+testEquality 0 _ _ = error "testEquality won't work with 0 iterations."
 testEquality x e1 e2 = do
-    (x',m1,m2) <- test e1 e2
-    if not x' then
-        return (False, (m1, m2))
-    else do
-        (rs, model) <- testEquality (x-1) e1 e2
-        return (x' && rs, model)
+  results <- mapM (const (test e1 e2)) [1..x]
+  let feedback = foldr add defFbCount (map fst results) -- sum of feedbacks
+  -- get list of counter models where
+  let counters = map snd (filter (not . equal . fst) results)
+  if null counters then
+    return (feedback, ([], M.empty))
+  else
+    return (feedback, head counters)
+
+test :: LExprTeacher -> LExprStudent -> IO (FeedbackCount, (Model, ArrayModel))
+test e1 e2 = do
+    ((CBool res1),(m,arrM,_)) <- testLExpr e1
+    evalInfo'                 <- expandEvalInfo e2 (m, arrM)
+    (CBool res2)              <- testModel e2 evalInfo'
+    let (primitivesModel, arrayModel, _) = evalInfo'
+    let fb = toFeedbackCount res1 res2
+    return (fb, (primitivesModel, arrayModel))
 
 -- Given an LExpr, generates a substitution model for all variables in it,
 -- and returns whether the formula evaluates to true or to false when that model

src/LogicIR/Backend/Z3/API.hs

 module LogicIR.Backend.Z3.API
        ( equivalentTo
        , showZ3AST
+       , timeoutTime
        )
        where
 
@@ -17,6 +18,10 @@ import LogicIR.Backend.Z3.Z3
 import LogicIR.Expr          (LExpr, lnot, (.&&), (.<==>))
 import Model
 
+-- The timeout time in milliseconds.
+timeoutTime :: Integer
+timeoutTime = 5000
+
 data Z3Response = Satisfiable Model | Unsatisfiable | Undecidable
                   deriving Show
 
@@ -100,7 +105,7 @@ catchTimeout prog = do
 -- | Z3 try evaluation with timeout.
 tryZ3 :: Z3 a -> IO a
 tryZ3 prog = do
-  env <- newEnv Nothing (  opt "timeout" (5000 :: Integer)
+  env <- newEnv Nothing (  opt "timeout" timeoutTime
                         +? opt "model_validate" True
                         +? opt "well_sorted_check" True
                         +? opt "auto_config" True