module Modelling.PetriNet.PetriDeadlock.Instance where

import qualified Data.Map                         as M (fromList)
import qualified Data.Set                         as S (fromList)

import Data.List.NonEmpty                 (NonEmpty((:|)))
import Modelling.PetriNet.Reach.Deadlock (DeadlockInstance (..))
import Modelling.PetriNet.Reach.Type    (Capacity (..), Net (..), State (..))
import Data.GraphViz.Commands           (GraphvizCommand (Circo))

examWs2024 :: DeadlockInstance String String
examWs2024 :: DeadlockInstance String String
examWs2024 = DeadlockInstance {
  drawUsing :: GraphvizCommand
drawUsing = GraphvizCommand
Circo,
  minLength :: Int
minLength = Int
14,
  noLongerThan :: Maybe Int
noLongerThan = Maybe Int
forall a. Maybe a
Nothing,
  petriNet :: Net String String
petriNet = Net {
    places :: Set String
places = [String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList [String
"s1", String
"s2", String
"s3", String
"s4", String
"s5", String
"s6"],
    transitions :: Set String
transitions = [String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList [String
"t1", String
"t2", String
"t3", String
"t4", String
"t5", String
"t6", String
"t7", String
"t8"],
    connections :: [Connection String String]
connections = [
      ([String
"s3"], String
"t1", [String
"s6"]),
      ([String
"s3"], String
"t2", [String
"s4", String
"s5"]),
      ([String
"s4"], String
"t3", [String
"s2"]),
      ([String
"s5"], String
"t4", [String
"s4"]),
      ([String
"s1"], String
"t5", [String
"s1"]),
      ([String
"s2"], String
"t6", [String
"s1", String
"s3"]),
      ([String
"s2", String
"s6"], String
"t7", [String
"s4", String
"s5"]),
      ([String
"s1"], String
"t8", [String
"s3"])
      ],
    capacity :: Capacity String
capacity = Capacity String
forall s. Capacity s
Unbounded,
    start :: State String
start = State {
      unState :: Map String Int
unState = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
        (String
"s1", Int
1),
        (String
"s2", Int
0),
        (String
"s3", Int
1),
        (String
"s4", Int
1),
        (String
"s5", Int
1),
        (String
"s6", Int
1)
        ]
      }
    },
  showPlaceNames :: Bool
showPlaceNames = Bool
False,
  maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
1,
  shortestSolutions :: Either (NonEmpty [String]) (NonEmpty [String])
shortestSolutions = NonEmpty [String] -> Either (NonEmpty [String]) (NonEmpty [String])
forall a b. a -> Either a b
Left ([] [String] -> [[String]] -> NonEmpty [String]
forall a. a -> [a] -> NonEmpty a
:| []), -- TO DO: add a solution here
  withLengthHint :: Maybe Int
withLengthHint = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
14,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
True,
  rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = Maybe Int
forall a. Maybe a
Nothing
  }