diff --git a/src/Modelling/PetriNet/Reach/Deadlock.hs b/src/Modelling/PetriNet/Reach/Deadlock.hs index 1616bf9c2..ab034397c 100644 --- a/src/Modelling/PetriNet/Reach/Deadlock.hs +++ b/src/Modelling/PetriNet/Reach/Deadlock.hs @@ -45,7 +45,7 @@ module Modelling.PetriNet.Reach.Deadlock ( exampleInstance, ) where -import qualified Data.Bimap as BM (lookup) +import qualified Data.Bimap as BM (fromList, lookup, memberR) import qualified Data.Map as M (fromList) import qualified Data.Set as S (fromList, toList) @@ -79,7 +79,7 @@ import Modelling.PetriNet.Reach.Reach ( provideSolutionsFeedback, validateDrawabilityAndSolutionFiltering, ) -import Modelling.PetriNet.Reach.Roll (netLimitsFiltered, simpleConnectionGenerator, generateValidConnection, generateFusableConnections) +import Modelling.PetriNet.Reach.Roll (netLimitsFiltered, simpleConnectionGenerator) import Modelling.PetriNet.Reach.Step (executes, successors) import Modelling.PetriNet.Reach.Type ( ArrowDensityConstraints(..), @@ -116,6 +116,7 @@ import Control.OutputCapable.Blocks.Generic ( ($>>), ($>>=), ) +import Data.Functor ((<&>)) import Data.Bifunctor (bimap) import Data.Either.Combinators (whenRight) import Control.Functor.Trans (FunctorTrans (lift)) @@ -123,6 +124,7 @@ import Control.Monad (guard) import Control.Monad.Catch (MonadCatch, MonadThrow) import Control.Monad.Extra (whenJust) import Control.Monad.Random (RandomGen, evalRandT, mkStdGen) +import System.Random.Shuffle (shuffleM) import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) import Control.Monad.Trans.Random (RandT) import Data.Maybe (fromMaybe) @@ -444,21 +446,47 @@ try conf = do if requiredFusableTransitionsConsuming == 0 && requiredFusableTransitionsProducing == 0 then return $ netLimitsFiltered simpleConnectionGenerator else do - (transitionConsumingBimap, transitionProducingBimap) <- - generateFusableConnections ps ts requiredFusableTransitionsConsuming requiredFusableTransitionsProducing + -- Generate pre-determined fusable node connections: + -- First, randomly select transitions and places for fusable nodes + shuffledTransitions <- shuffleM ts + shuffledPlaces <- shuffleM ps + let (inputFusableTransitions, remainingTransitions) = splitAt requiredFusableTransitionsConsuming shuffledTransitions + outputFusableTransitions = take requiredFusableTransitionsProducing remainingTransitions + (placesForInputFusableTransitions, remainingPlaces) = splitAt requiredFusableTransitionsConsuming shuffledPlaces + placesForOutputFusableTransitions = take requiredFusableTransitionsProducing remainingPlaces + -- Next, create bimaps from fusable transitions to their fusion-relevant places + let transitionConsumingBimap = BM.fromList $ zip inputFusableTransitions placesForInputFusableTransitions + transitionProducingBimap = BM.fromList $ zip outputFusableTransitions placesForOutputFusableTransitions + -- Helpers for generating valid connections: + let isValidInputPlaceUsage = + if requiredFusableTransitionsConsuming == 0 + then \_ _ -> True + else \vor nach -> + -- For each place in vor: if it's a forbidden input place, only allow if vor == nach == [that place] + all (\place -> not (BM.memberR place transitionConsumingBimap) || (vor == [place] && nach == [place])) vor + isValidOutputPlaceUsage = + if requiredFusableTransitionsProducing == 0 + then \_ _ -> True + else \nach vor -> + -- For each place in nach: if it's a forbidden output place, only allow if vor == nach == [that place] + all (\place -> not (BM.memberR place transitionProducingBimap) || (vor == [place] && nach == [place])) nach return $ netLimitsFiltered - $ \inputPlacesAction outputPlacesAction t -> do - (vor, nach) <- generateValidConnection transitionConsumingBimap transitionProducingBimap inputPlacesAction outputPlacesAction t - case BM.lookup t transitionConsumingBimap of - Just preVor - -> return (preVor : vor, t, nach) - _ - -> case BM.lookup t transitionProducingBimap of - Just preNach - -> return (vor, t, preNach : nach) - _ - -> return (vor, t, nach) - -- impossible for both lookups to return Just + $ \inputPlacesAction outputPlacesAction t -> + -- Generate a valid connection for a transition, with retry logic + let + vorAction = case BM.lookup t transitionConsumingBimap of + Just preVor -> return ([preVor], [], notElem preVor) -- If t has a pregenerated input place, prevent that place from appearing in nach + _ -> inputPlacesAction <&> \vor -> (vor, vor, isValidInputPlaceUsage vor) + nachAction = case BM.lookup t transitionProducingBimap of + Just preNach -> return ([preNach], [], notElem preNach) -- If t has a pregenerated output place, prevent that place from appearing in vor + _ -> outputPlacesAction <&> \nach -> (nach, nach, isValidOutputPlaceUsage nach) + go = do + (vor, vorForCheck, checkInputPlaceUsage) <- vorAction + (nach, nachForCheck, checkOutputPlaceUsage) <- nachAction + if checkInputPlaceUsage nachForCheck && checkOutputPlaceUsage vorForCheck + then return (vor, t, nach) + else go -- Retry if invalid + in go n <- MaybeT $ netGenerator (arrowDensityConstraints conf) (numPlaces conf) diff --git a/src/Modelling/PetriNet/Reach/Roll.hs b/src/Modelling/PetriNet/Reach/Roll.hs index cba41cf19..20ec69d97 100644 --- a/src/Modelling/PetriNet/Reach/Roll.hs +++ b/src/Modelling/PetriNet/Reach/Roll.hs @@ -4,16 +4,8 @@ originally from Autotool (https://gitlab.imn.htwk-leipzig.de/autotool/all0) based on revision: ad25a990816a162fdd13941ff889653f22d6ea0a based on file: collection/src/Petri/Roll.hs -} -module Modelling.PetriNet.Reach.Roll (netLimitsFiltered, simpleConnectionGenerator, generateValidConnection, generateFusableConnections) where +module Modelling.PetriNet.Reach.Roll (netLimitsFiltered, simpleConnectionGenerator) where -import qualified Data.Bimap as BM ( - fromList, - lookup, - member, - memberR, - null, - Bimap, - ) import qualified Data.Map as M ( fromList, fromListWith, @@ -39,51 +31,6 @@ import Control.Monad.Random.Class (MonadRandom (getRandomR)) import Data.Maybe (fromMaybe) import System.Random.Shuffle (shuffleM) --- | Generate a valid connection for a transition with retry logic -generateValidConnection - :: (MonadRandom m, Ord s, Ord t) - => BM.Bimap t s -- ^ Bimap from fusable consuming-transitions to their input places - -> BM.Bimap t s -- ^ Bimap from fusable consuming-transitions to their output places - -> m [s] -- ^ Action to get input places - -> m [s] -- ^ Action to get output places - -> t -- ^ Transition - -> m ([s], [s]) -- ^ (vor, nach) -generateValidConnection transitionConsumingBimap transitionProducingBimap = - \inputPlacesAction outputPlacesAction t -> - let - go = do - vor <- if BM.member t transitionConsumingBimap - then return [] - else inputPlacesAction - nach <- if BM.member t transitionProducingBimap - then return [] - else outputPlacesAction - -- Check both input and output place usage - if isValidInputPlaceUsage t vor nach && isValidOutputPlaceUsage t vor nach - then return (vor, nach) - else go -- Retry if invalid - in go - where - -- | Check if input place usage is valid for a transition - isValidInputPlaceUsage = - if BM.null transitionConsumingBimap - then \_ _ _ -> True - else \t vor nach -> - -- For each place in vor: if it's a forbidden input place, only allow if vor == nach == [that place] - all (\place -> not (BM.memberR place transitionConsumingBimap) || (vor == [place] && nach == [place])) vor - -- If t has a pregenerated input place, prevent that place from appearing in nach - && maybe True (`notElem` nach) (BM.lookup t transitionConsumingBimap) - - -- | Check if output place usage is valid for a transition - isValidOutputPlaceUsage = - if BM.null transitionProducingBimap - then \_ _ _ -> True - else \t vor nach -> - -- For each place in nach: if it's a forbidden output place, only allow if vor == nach == [that place] - all (\place -> not (BM.memberR place transitionProducingBimap) || (vor == [place] && nach == [place])) nach - -- If t has a pregenerated output place, prevent that place from appearing in vor - && maybe True (`notElem` vor) (BM.lookup t transitionProducingBimap) - state :: (MonadRandom m, Ord s) => [s] -> m (State s) state ps = do qs <- selection ps @@ -113,30 +60,6 @@ inBounds :: (Int, Maybe Int) -> Int -> Bool inBounds (low, maybeHigh) value = value >= low && maybe True (value <=) maybeHigh --- | Generate pre-determined fusable node connections -generateFusableConnections - :: (MonadRandom m, Ord t, Ord s) - => [s] -- ^ All places - -> [t] -- ^ All transitions - -> Int -- ^ Number of fusable consuming-transitions to create - -> Int -- ^ Number of fusable producing-transitions to create - -> m (BM.Bimap t s, BM.Bimap t s) -generateFusableConnections allPlaces allTransitions numConsumingFusable numProducingFusable = do - -- Randomly select transitions and places for fusable nodes - shuffledTransitions <- shuffleM allTransitions - shuffledPlaces <- shuffleM allPlaces - let (inputFusableTransitions, remainingTransitions) = splitAt numConsumingFusable shuffledTransitions - outputFusableTransitions = take numProducingFusable remainingTransitions - (placesForInputFusableTransitions, remainingPlaces) = splitAt numConsumingFusable shuffledPlaces - placesForOutputFusableTransitions = take numProducingFusable remainingPlaces - -- Create bimaps from transitions to their pregenerated places - let transitionConsumingBimap = BM.fromList $ zip inputFusableTransitions placesForInputFusableTransitions - transitionProducingBimap = BM.fromList $ zip outputFusableTransitions placesForOutputFusableTransitions - -- Return transition-place bimaps - return ( transitionConsumingBimap -- bimap from fusable consuming-transitions to their places - , transitionProducingBimap -- bimap from fusable producing-transitions to their places - ) - -- | Generate a net with limits and filtering for isolated nodes and transition behaviour constraints, -- potentially with pregenerated fusable connections (of which the makeUpdateConnection argument takes care) netLimitsFiltered