Removed firing vector argument from cut construction

src/Main.hs

@@ -360,7 +360,7 @@ findLivenessRefinementByEmptyTraps net m x traps = do
                 rm <- refineSafetyProperty net FTrue traps m
                 case rm of
                     (Nothing, _) -> do
-                        cut <- generateLivenessRefinement net x traps
+                        cut <- generateLivenessRefinement net traps
                         return $ Just cut
                     (Just _, _) ->
                         return Nothing
@@ -370,14 +370,14 @@ findLivenessRefinementByEmptyTraps net m x traps = do
                             checkSafetyProperty' net FTrue traps'
                 case rm of
                     (Nothing, _) -> do
-                        cut <- generateLivenessRefinement net x traps'
+                        cut <- generateLivenessRefinement net traps'
                         return $ Just cut
                     (Just m', _) ->
                         findLivenessRefinementByEmptyTraps net m' x traps'
 
-generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
-generateLivenessRefinement net x traps = do
-        let cut = constructCut net x traps
+generateLivenessRefinement :: PetriNet -> [Trap] -> OptIO Cut
+generateLivenessRefinement net traps = do
+        let cut = constructCut net traps
         verbosePut 3 $ "- cut: " ++ show cut
         return cut
 

src/PetriNet.hs

@@ -99,8 +99,8 @@ instance Show PetriNet where
                           show l ++ " -> " ++ show s ++ " -> " ++ show r
 
 -- TODO: better cuts, scc, min cut?
-constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
-constructCut net _ traps = (trapComponents, trapOutputs)
+constructCut:: PetriNet -> [Trap] -> Cut
+constructCut net traps = (trapComponents, trapOutputs)
         where trapComponent trap = (sort trap, sort (mpre net trap) \\ trapOutputs)
               trapComponents = listSet $ map trapComponent traps
               trapOutput trap = mpost net trap \\ mpre net trap

src/Solver/SComponent.hs

@@ -101,5 +101,5 @@ cutFromAssignment net x p' t' y =
             s1 = filter (\p -> val p' p > 0) $ mpre net t1
             s2 = filter (\p -> val p' p > 0) $ mpre net t2
             size = fromIntegral $ M.size $ M.filter (> 0) p'
-        in  (constructCut net x [s1,s2], size)
+        in  (constructCut net [s1,s2], size)
 

src/Solver/TransitionInvariant.hs

 module Solver.TransitionInvariant
-    (checkTransitionInvariantSat)
+    (checkTransitionInvariantSat
+    ,checkTransitionInvariant
+    ,tInvariantConstraints
+    ,nonnegativityConstraints)
 where
 
 import Data.SBV
@@ -32,12 +35,16 @@ checkCuts cuts x = bAnd $ map checkCut cuts
                       cPost = map (positiveVal x) u
                   in  bAnd cPre ==> bOr cPost
 
-checkTransitionInvariant :: PetriNet -> Formula Transition ->
-        [Cut] -> SIMap Transition -> SBool
-checkTransitionInvariant net f cuts x =
+checkTransitionInvariant :: PetriNet -> SIMap Transition -> SBool
+checkTransitionInvariant net x =
         tInvariantConstraints net x &&&
         nonnegativityConstraints x &&&
-        finalInvariantConstraints x &&&
+        finalInvariantConstraints x
+
+checkTransitionInvariantMethod :: PetriNet -> Formula Transition ->
+        [Cut] -> SIMap Transition -> SBool
+checkTransitionInvariantMethod net f cuts x =
+        checkTransitionInvariant net x &&&
         checkCuts cuts x &&&
         evaluateFormula f x
 
@@ -47,7 +54,7 @@ checkTransitionInvariantSat net f cuts =
         let x = makeVarMap $ transitions net
         in  ("transition invariant constraints", "transition invariant",
             getNames x,
-            \fm -> checkTransitionInvariant net f cuts (fmap fm x),
+            \fm -> checkTransitionInvariantMethod net f cuts (fmap fm x),
             \fm -> firingVectorFromAssignment (fmap fm x))
 
 firingVectorFromAssignment :: IMap Transition -> FiringVector