Added trap refinement

src/Main.hs

@@ -9,12 +9,25 @@ import Solver
 
 checkProperty :: PetriNet -> Property -> IO ()
 checkProperty net p = do
-        r <- checkPropertyConstraintsSat net p
+        r <- checkPropertyConstraintsSat net p []
         case r of
             Nothing -> putStrLn "Property satisfied"
-            Just m -> putStrLn "Property not satisfied, model:" >> print m
+            Just m -> putStrLn "Property may not satisfied, model:" >> print m
 
---checkPropertyWithTrapRefinement :: PetriNet -> Property -> IO ()
+checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
+checkPropertyWithTrapRefinement net p traps = do
+        r <- checkPropertyConstraintsSat net p traps
+        case r of
+            Nothing -> putStrLn "Property satisfied"
+            Just m -> do
+                putStrLn "Property not satisfied, model:" >> print m
+                r2 <- checkTrapConstraintsSat net m
+                case r2 of
+                    Nothing -> putStrLn "No trap found"
+                    Just m2 -> do
+                        let trap = map fst $ filter snd m2
+                        putStrLn "Trap found:" >> print trap
+                        checkPropertyWithTrapRefinement net p (trap:traps)
 
 main :: IO ()
 main = do
@@ -26,6 +39,6 @@ main = do
         putStrLn $ "Analyzing " ++ showName net
         mapM_ (\p -> do
                   putStrLn $ "Checking " ++ show p
-                  checkProperty net p
+                  checkPropertyWithTrapRefinement net p []
               ) properties
 

src/Solver.hs

@@ -11,7 +11,7 @@ import Property
 type ModelSI = M.Map String SInteger
 type ModelSB = M.Map String SBool
 type ModelI = M.Map String Integer
-type ModelB = M.Map String Bool
+--type ModelB = M.Map String Bool
 type ModelLI = [(String, Integer)]
 type ModelLB = [(String, Bool)]
 
@@ -73,21 +73,26 @@ checkTrapConstraints m net =
 
 checkTrapMarked :: ModelSB -> PetriNet -> SBool
 checkTrapMarked m net =
-        let marked = map fst $ filter (( > 0) . snd) $ (initials net)
+        let marked = map fst $ filter (( > 0) . snd) $ initials net
         in  bOr $ map (m M.!) marked
 
-checkTrapUnassigned :: ModelSB -> ModelI -> SBool
-checkTrapUnassigned mt ma =
-        let assigned = map fst $ filter (( > 0) . snd) $ M.toList ma
+checkTrapUnassigned :: ModelSB -> ModelI -> PetriNet -> SBool
+checkTrapUnassigned mt ma net =
+        let assigned = filter (( > 0) . (ma M.!)) $ places net
         in  bAnd $ map (bnot . (mt M.!)) assigned
 
 checkAllTrapConstraints :: ModelSB -> ModelI -> PetriNet -> SBool
 checkAllTrapConstraints mt ma net =
         let tc = checkTrapConstraints mt net
             tm = checkTrapMarked mt net
-            tu = checkTrapUnassigned mt ma
+            tu = checkTrapUnassigned mt ma net
         in  tc &&& tm &&& tu
 
+checkTrapDeltaConstraints :: ModelSI -> [String] -> SBool
+checkTrapDeltaConstraints m trap =
+        let tokens = map (m M.!) trap
+        in  sum tokens .>= 1
+
 checkPropertyConstraints :: ModelSI -> PetriNet -> Property -> SBool
 checkPropertyConstraints m net p =
         let netConstraints = case ptype p of
@@ -97,6 +102,13 @@ checkPropertyConstraints m net p =
             propertyConstraint = evaluateFormula m (pformula p)
         in  netConstraints &&& nonnegativityConstraint &&& propertyConstraint
 
+checkPropertyPlusTrapConstraints :: ModelSI -> PetriNet -> Property ->
+        [[String]] -> SBool
+checkPropertyPlusTrapConstraints m net p traps =
+        let propConstraints = checkPropertyConstraints m net p
+            trapConstraints = map (checkTrapDeltaConstraints m) traps
+        in  propConstraints &&& bAnd trapConstraints
+
 symConstraints :: SymWord a => [String] -> ([(String, SBV a)] -> SBool) ->
         Symbolic SBool
 symConstraints vars constraint = do
@@ -114,15 +126,15 @@ checkSat vars constraint = do
         result <- sat $ symConstraints vars constraint
         return $ rebuildModel vars $ getModel result
 
-checkPropertyConstraintsSat :: PetriNet -> Property -> IO (Maybe ModelLI)
-checkPropertyConstraintsSat net p =
+checkPropertyConstraintsSat :: PetriNet -> Property -> [[String]] -> IO (Maybe ModelLI)
+checkPropertyConstraintsSat net p traps =
         let vars = places net ++ transitions net
-            cons m = checkPropertyConstraints (M.fromList m) net p
+            cons m = checkPropertyPlusTrapConstraints (M.fromList m) net p traps
         in  checkSat vars cons
 
-checkTrapConstraintsSat :: PetriNet -> ModelI -> IO (Maybe ModelLB)
+checkTrapConstraintsSat :: PetriNet -> ModelLI -> IO (Maybe ModelLB)
 checkTrapConstraintsSat net ma =
-        let vars = transitions net
-            cons m = checkAllTrapConstraints (M.fromList m) ma net
+        let vars = places net
+            cons m = checkAllTrapConstraints (M.fromList m) (M.fromList ma) net
         in  checkSat vars cons