Fix detection of Marabou timeouts

ChangeLog.md

@@ -1,5 +1,9 @@
 # Changelog for Vehicle
 
+## Version 0.16.1
+
+* Fixed detection of Marabou timeouts.
+
 ## Version 0.16
 
 * Decreased type-checking time by ~50%

vehicle/src/Vehicle/Verify/Specification/IO.hs

@@ -447,7 +447,6 @@ verifyQuery queryMetaData@(QueryMetaData queryAddress metaNetwork reconstruction
     (verifierSettings, verificationCache, progressBar) <- ask
     let queryFile = calculateQueryFileName verificationCache queryAddress
 
-    tell (Sum 1)
     errorOrResult <- runExceptT $ do
       result <- invokeVerifier verifierSettings metaNetwork queryFile
       liftIO $ incProgress progressBar 1
@@ -467,7 +466,9 @@ verifyQuery queryMetaData@(QueryMetaData queryAddress metaNetwork reconstruction
 
     case errorOrResult of
       Left err -> throwError (queryMetaData, err)
-      Right result -> return result
+      Right result -> do
+        tell (Sum 1)
+        return result
 
 invokeVerifier ::
   (MonadVerifyQuery m) =>
@@ -575,8 +576,28 @@ outputPropertyResult ::
   m ()
 outputPropertyResult verifierSettings verificationCache address result = do
   let VerifierSettings {..} = verifierSettings
-  VIO.writeStdoutLn (layoutAsText $ "    result: " <> pretty result)
+
+  -- Write the result to the cache
   writePropertyResult verificationCache address (isVerified result)
+
+  -- Print result to command line
+  let verifierName = pretty (verifierID verifier)
+  let (verified, evidenceText) = case result of
+        PropertyCompleted maybeResult -> do
+          case maybeResult of
+            Trivial status -> (Just status, "(trivial)")
+            NonTrivial (negated, status) -> do
+              let witnessText = if negated then "counterexample" else "witness"
+              case status of
+                UnSAT -> (Just negated, verifierName <+> "proved no" <+> witnessText <+> "exists")
+                SAT Nothing -> (Just (not negated), verifierName <+> "found no" <> witnessText)
+                SAT Just {} -> (Just (not negated), verifierName <+> "found a" <+> witnessText)
+        PropertyErrored (_, err) -> do
+          let cause = if isTimeoutError err then "timed out" else "errored"
+          (Nothing, verifierName <+> cause)
+  VIO.writeStdoutLn (layoutAsText $ "    result: " <> pretty (statusSymbol verified) <+> "-" <+> evidenceText)
+
+  -- Output any additional information
   case result of
     PropertyCompleted status -> case status of
       NonTrivial (_, SAT (Just (UserVariableAssignment assignments))) -> do

vehicle/src/Vehicle/Verify/Specification/Status.hs

@@ -2,7 +2,6 @@ module Vehicle.Verify.Specification.Status where
 
 import Data.List.Split (chunksOf)
 import Data.Set (Set)
-import Data.Text (Text)
 import System.Console.ANSI (Color (..))
 import Vehicle.Compile.Prelude
 import Vehicle.Data.Builtin.Standard
@@ -56,33 +55,17 @@ instance IsVerified PropertyStatus where
       NonTrivial (negated, result) -> evaluateQuery negated result
     PropertyErrored {} -> False
 
-instance Pretty PropertyStatus where
-  pretty propertyStatus = do
-    let (verified, evidenceText) = case propertyStatus of
-          PropertyCompleted maybeResult -> do
-            case maybeResult of
-              Trivial status -> (status, "(trivial)")
-              NonTrivial (negated, status) -> do
-                let witnessText = if negated then "counterexample" else "witness"
-                case status of
-                  UnSAT -> (negated, "proved no" <+> witnessText <+> "exists")
-                  SAT Nothing -> (not negated, "no" <> witnessText <+> "found")
-                  SAT Just {} -> (not negated, witnessText <+> "found")
-          PropertyErrored (_, err) -> (False, if isTimeoutError err then "verifier timed out" else "verifier errored")
-    pretty (statusSymbol verified) <+> "-" <+> evidenceText
-
 --------------------------------------------------------------------------------
 -- Verification status of a multi property
 
-statusSymbol :: Bool -> String
+statusSymbol :: Maybe Bool -> String
 statusSymbol verified = do
-  let (colour, symbol) = if verified then (Green, "🗸") else (Red, "✗")
+  let (colour, symbol) = case verified of
+        Just True -> (Green, "🗸")
+        Nothing -> (Yellow, "?")
+        Just False -> (Red, "✗")
   setTextColour colour symbol
 
-prettyNameAndStatus :: Text -> Bool -> Doc a
-prettyNameAndStatus name verified = do
-  pretty (statusSymbol verified) <+> pretty name
-
 prettyUserVariableAssignment :: (Name, RationalTensor) -> Doc a
 prettyUserVariableAssignment (var, variableValue) =
   pretty var <> ":" <+> pretty variableValue

vehicle/src/Vehicle/Verify/Verifier/Core.hs

@@ -25,7 +25,7 @@ data VerifierID
 instance Show VerifierID where
   show = \case
     Marabou -> "Marabou"
-    TestVerifier -> "Test"
+    TestVerifier -> "TestVerifier"
 
 instance Pretty VerifierID where
   pretty = pretty . show

vehicle/src/Vehicle/Verify/Verifier/Marabou.hs

@@ -36,11 +36,13 @@ prepareMarabouArgs metaNetwork queryFile = case metaNetwork of
 parseMarabouOutput :: ParseVerifierOutput
 parseMarabouOutput output = do
   let outputLines = fmap Text.pack (lines output)
-  let resultIndex = findIndex (\v -> v == "sat" || v == "unsat" || v == "timeout") outputLines
+  let resultIndex = findIndex (\v -> v == "sat" || v == "unsat" || v == "Timeout") outputLines
   case resultIndex of
-    Nothing -> throwError $ VerifierOutputMalformed "Cannot find 'sat' or 'unsat'"
+    Nothing -> do
+      logDebug MinDetail $ pretty output
+      throwError $ VerifierOutputMalformed "Cannot find 'sat', 'unsat' or 'timeout'"
     Just i
-      | outputLines !! i == "timeout" -> throwError VerifierTimedOut
+      | outputLines !! i == "Timeout" -> throwError VerifierTimedOut
       | outputLines !! i == "unsat" -> return UnSAT
       | otherwise -> do
           let assignmentOutput = drop (i + 1) outputLines

vehicle/tests/golden/compile/acasXu/MarabouVerify.out.golden

@@ -1,4 +1,4 @@
 Verifying properties:
   property3 [......................................................] 0/1 queries  property3 [======================================================] 1/1 queries
-    result: ✗ - counterexample found
-      x: [ 1799.988667, 5.2420604112e-2, 3.09999732192, 980.0, 1055.5284 ]
+    result: ✗ - Marabou found a counterexample
+      x: [ 1799.988667, 5.9998124016e-2, 3.09999732192, 980.0, 1089.0516 ]

vehicle/tests/golden/compile/issue641/MarabouVerify.err.golden

@@ -6,7 +6,8 @@ In order to provide support, Vehicle has automatically converted the strict ineq
 See https://github.com/vehicle-lang/vehicle/issues/74 for further details.
 
 
-Warning: In property 'p', in queries 1 and 2 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries.
+Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are:
+  - queries 1 and 2
 
 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.
 

vehicle/tests/golden/compile/issue641/MarabouVerify.out.golden

@@ -1,4 +1,4 @@
 Verifying properties:
   p [..............................................................] 0/2 queries  p [===============================>..............................] 1/2 queries  p [==============================================================] 2/2 queries
-    result: 🗸 - witness found
+    result: 🗸 - Marabou found a witness
 

vehicle/tests/golden/compile/simple-fourierMotzkin/TestVerify.out.golden

@@ -1,4 +1,4 @@
 Verifying properties:
   underConstrainedVars [...........................................] 0/1 queries  underConstrainedVars [===========================================] 1/1 queries
-    result: 🗸 - witness found
+    result: 🗸 - TestVerifier found a witness
       x: [ -9.3, 9.5, -1.0, 3.0, 0.0 ]

vehicle/tests/golden/compile/windController/MarabouVerify.out.golden

@@ -1,3 +1,3 @@
 Verifying properties:
   safe [...........................................................] 0/2 queries  safe [=============================>.............................] 1/2 queries  safe [===========================================================] 2/2 queries
-    result: 🗸 - proved no counterexample exists
+    result: 🗸 - Marabou proved no counterexample exists

vehicle/tests/golden/compile/windController/TestVerify.out.golden

@@ -1,4 +1,4 @@
 Verifying properties:
   safe [...........................................................] 0/2 queries
-    result: ✗ - counterexample found
+    result: ✗ - TestVerifier found a counterexample
       x: [ -2.4, -1.6 ]

vehicle/tests/golden/error/other-verifier/verifierTimeout/TestVerify.out.golden

@@ -1,3 +1,5 @@
 Verifying properties:
-  p1 [.............................................................] 0/1 queries    result: ✗ - verifier timed out
-  p2 [.............................................................] 0/1 queries    result: ✗ - verifier timed out
+  p1 [.............................................................] 0/1 queries
+    result: ? - TestVerifier timed out
+  p2 [.............................................................] 0/1 queries
+    result: ? - TestVerifier timed out