Added timeout handling and stopped individual property errors being f…

…atal (#870)

* Added timeout handling and made it so properties continue to be verified if there is an error

* Add CHANGELOG

* Fixed import bug

* Add printing of stats

ChangeLog.md

@@ -8,8 +8,15 @@
 
 * Improved the ordering of constraints in generated query files.
 
+* Added better handling of verifier timeouts.
+
+* If a verifier throws an error whilst verifying a property, Vehicle will now continue to try
+  verify the other properties in the file instead of immediately exiting.
+
 * When multiple similar warnings are thrown at different indices of the same property vector (i.e. properties of type `Vector Bool n`), they are now collapsed into a single warning.
 
+* When Vehicle has finished verifying a vector of properties, Vehicle will now output the stats about the number verified, falsified, timed-out and errored.
+
 ## Version 0.15
 
 * Added functions `min` and `max` over rationals.

vehicle/src/Vehicle/Verify/Core.hs

@@ -10,7 +10,7 @@ import Data.Map (Map)
 import Data.Text (Text, unpack)
 import GHC.Generics (Generic)
 import Prettyprinter (brackets)
-import System.FilePath ((<.>))
+import System.FilePath ((<.>), (</>))
 import Vehicle.Compile.Resource
 import Vehicle.Data.Builtin.Core
 import Vehicle.Data.QuantifiedVariable (NetworkElementVariable)
@@ -137,9 +137,13 @@ type QueryID = Int
 
 type QueryAddress = (PropertyAddress, QueryID)
 
-calculateQueryFileName :: QueryAddress -> FilePath
-calculateQueryFileName (propertyAddress, queryID) = do
-  calculatePropertyFilePrefix propertyAddress <> "-query" <> show queryID <.> "txt"
+calculateQueryFileName :: FilePath -> QueryAddress -> FilePath
+calculateQueryFileName verificationCache (propertyAddress, queryID) = do
+  verificationCache
+    </> calculatePropertyFilePrefix propertyAddress
+      <> "-query"
+      <> show queryID
+        <.> "txt"
 
 --------------------------------------------------------------------------------
 -- Queries
@@ -164,15 +168,3 @@ createNetworkVarName networkName application inputOrOutput =
   pretty networkName
     <> pretty (fmap subscript (show application))
     <> brackets (pretty inputOrOutput)
-
---------------------------------------------------------------------------------
--- Network assignments
-
-{-
-instance Pretty NetworkVariableAssignment where
-  pretty (NetworkVariableAssignment assignment) = do
-    vsep (prettyVariable <$> Map.toList assignment)
-    where
-      prettyVariable :: (NetworkVerifierVariable, Rational) -> Doc a
-      prettyVariable (var, value) = "x" <> pretty var <> ":" <+> pretty value
--}

vehicle/src/Vehicle/Verify/Specification.hs

@@ -152,7 +152,7 @@ specificationPropertyNames (Specification properties) = fmap fst properties
 -- verification of an entire specification.
 data SpecificationCacheIndex = SpecificationCacheIndex
   { resourcesIntegrityInfo :: ResourcesIntegrityInfo,
-    properties :: [(Name, MultiProperty ())]
+    properties :: [(PropertyName, MultiProperty ())]
   }
   deriving (Generic)