From 5baa10630be152c869bf9e150008d908d50235f7 Mon Sep 17 00:00:00 2001 From: Eneas Rotterdam Date: Mon, 23 Mar 2026 10:42:02 +0100 Subject: [PATCH 1/2] Add example solutions to default instances for `Reach` and `Deadlock` --- example/src/Modelling/PetriNet/PetriDeadlock/Instance.hs | 5 ++++- example/src/Modelling/PetriNet/PetriReach/Instance.hs | 6 +++++- src/Modelling/PetriNet/Reach/Deadlock.hs | 7 +++++-- src/Modelling/PetriNet/Reach/Reach.hs | 8 ++++++-- 4 files changed, 20 insertions(+), 6 deletions(-) diff --git a/example/src/Modelling/PetriNet/PetriDeadlock/Instance.hs b/example/src/Modelling/PetriNet/PetriDeadlock/Instance.hs index 92d258bcc..564d419a1 100644 --- a/example/src/Modelling/PetriNet/PetriDeadlock/Instance.hs +++ b/example/src/Modelling/PetriNet/PetriDeadlock/Instance.hs @@ -40,7 +40,10 @@ examWs2024 = DeadlockInstance { }, showPlaceNames = False, maxDisplayedSolutions = 1, - shortestSolutions = Left ([] :| []), -- TO DO: add a solution here + shortestSolutions = Left ([ + "t4", "t3", "t3", "t6", "t6", "t8", "t8", + "t8", "t1", "t1", "t1", "t1", "t1", "t1" + ] :| []), withLengthHint = Just 14, withMinLengthHint = True, rejectSpaceballsLength = Nothing diff --git a/example/src/Modelling/PetriNet/PetriReach/Instance.hs b/example/src/Modelling/PetriNet/PetriReach/Instance.hs index a3a178f82..fe6f39d4a 100644 --- a/example/src/Modelling/PetriNet/PetriReach/Instance.hs +++ b/example/src/Modelling/PetriNet/PetriReach/Instance.hs @@ -47,7 +47,11 @@ task5 = ReachInstance { showGoalNet = True, showPlaceNames = False, maxDisplayedSolutions = 1, - shortestSolutions = Left ([] :| []), -- TO DO: add a solution here + shortestSolutions = Left ([ + "t5", "t2", "t4", "t3", + "t5", "t2", "t4", "t3", + "t5", "t2", "t4", "t3" + ] :| []), withLengthHint = Just 12, withMinLengthHint = True, rejectSpaceballsLength = Nothing diff --git a/src/Modelling/PetriNet/Reach/Deadlock.hs b/src/Modelling/PetriNet/Reach/Deadlock.hs index 1616bf9c2..987eb704a 100644 --- a/src/Modelling/PetriNet/Reach/Deadlock.hs +++ b/src/Modelling/PetriNet/Reach/Deadlock.hs @@ -323,8 +323,11 @@ defaultDeadlockInstance = DeadlockInstance { noLongerThan = Nothing, petriNet = fst example, showPlaceNames = False, - maxDisplayedSolutions = 0, - shortestSolutions = Left ([] :| []), -- TO DO: add a solution + maxDisplayedSolutions = 1, + shortestSolutions = Left ([ + Transition 3, Transition 3, Transition 3, + Transition 2, Transition 2, Transition 2 + ] :| []), -- TO DO: add a solution withLengthHint = Just 9, withMinLengthHint = True, rejectSpaceballsLength = Nothing diff --git a/src/Modelling/PetriNet/Reach/Reach.hs b/src/Modelling/PetriNet/Reach/Reach.hs index 66cf03eca..31d7dc50c 100644 --- a/src/Modelling/PetriNet/Reach/Reach.hs +++ b/src/Modelling/PetriNet/Reach/Reach.hs @@ -616,8 +616,12 @@ defaultReachInstance = ReachInstance { noLongerThan = Nothing, showGoalNet = True, showPlaceNames = False, - maxDisplayedSolutions = 0, - shortestSolutions = Left ([] :| []), -- TO DO: add a solution + maxDisplayedSolutions = 1, + shortestSolutions = Left ([ + Transition 3, Transition 3, Transition 2, Transition 1, Transition 4, + Transition 3, Transition 3, Transition 2, Transition 1, Transition 4, + Transition 3, Transition 2 + ] :| []), withLengthHint = Just 12, withMinLengthHint = False, rejectSpaceballsLength = Nothing From c07b0fa2d480f5f7ed537ef23381d9efe52cf3ac Mon Sep 17 00:00:00 2001 From: Eneas Rotterdam Date: Mon, 23 Mar 2026 10:50:55 +0100 Subject: [PATCH 2/2] Remove now obsolete todo comment --- src/Modelling/PetriNet/Reach/Deadlock.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Modelling/PetriNet/Reach/Deadlock.hs b/src/Modelling/PetriNet/Reach/Deadlock.hs index 987eb704a..19f634d9e 100644 --- a/src/Modelling/PetriNet/Reach/Deadlock.hs +++ b/src/Modelling/PetriNet/Reach/Deadlock.hs @@ -327,7 +327,7 @@ defaultDeadlockInstance = DeadlockInstance { shortestSolutions = Left ([ Transition 3, Transition 3, Transition 3, Transition 2, Transition 2, Transition 2 - ] :| []), -- TO DO: add a solution + ] :| []), withLengthHint = Just 9, withMinLengthHint = True, rejectSpaceballsLength = Nothing