From 3afab48323ab450f313aa00c720133d7774fb302 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 4 Feb 2020 12:45:05 +0100 Subject: [PATCH] [#328] [stbx-core] split Transition module from WiringTree --- stbx-core/src/Statebox/Core/Transition.purs | 68 +++++++++++++++++++++ stbx-core/src/Statebox/Core/WiringTree.purs | 34 ++--------- stbx-protocol/spago.dhall | 4 +- 3 files changed, 77 insertions(+), 29 deletions(-) create mode 100644 stbx-core/src/Statebox/Core/Transition.purs diff --git a/stbx-core/src/Statebox/Core/Transition.purs b/stbx-core/src/Statebox/Core/Transition.purs new file mode 100644 index 00000000..272c1439 --- /dev/null +++ b/stbx-core/src/Statebox/Core/Transition.purs @@ -0,0 +1,68 @@ +module Statebox.Core.Transition where + +import Prelude +import Data.Array ((:)) +import Data.Foldable (foldr) +import Data.FoldableWithIndex (foldrWithIndex) +import Data.Map as Map +import Data.Maybe (Maybe(..)) + +import Data.ArrayMultiset (ArrayMultiset) +import Statebox.Core.Execution (Path) +import Statebox.Core.Types (PID, TID) + +-- TODO: these types are currently duplicated from Data.Petrinet.Representation.Dict +type TransitionF p tok = + { pre :: Array (PlaceMarkingF p tok) + , post :: Array (PlaceMarkingF p tok) + } + +type PlaceMarkingF p tok = + { place :: p + , tokens :: tok + } + +buildTokens :: ∀ a. Ord a => ArrayMultiset a -> ArrayMultiset a -> TransitionF a Int +buildTokens pre post = + { pre : buildPlaceMarkings pre + , post : buildPlaceMarkings post + } + +buildPlaceMarkings :: ∀ a. Ord a => ArrayMultiset a -> Array (PlaceMarkingF a Int) +buildPlaceMarkings multiset = + let map = foldr (Map.update (Just <<< (_ + 1))) Map.empty multiset + in foldrWithIndex (\place count -> (:) { place: place, tokens: count }) [] map + +type Tokens = Int + +type Transition = + { path :: Path + , transition :: TID + , name :: String + , tokens :: TransitionF PID Tokens + } + +data Glued a + = Untouched a + | Initial a + | Final a + | Glued a a + +isInitial :: ∀ a. Glued a -> Boolean +isInitial = case _ of + Initial a -> true + _ -> false + +isFinal :: ∀ a. Glued a -> Boolean +isFinal = case _ of + Final a -> true + _ -> false + +gluedTokens :: Glued Transition -> TransitionF PID Tokens +gluedTokens = case _ of + Untouched transition -> transition.tokens + Initial transition -> transition.tokens + Final transition -> transition.tokens + Glued transition1 transition2 -> { pre : transition1.tokens.pre + , post: transition2.tokens.post + } diff --git a/stbx-core/src/Statebox/Core/WiringTree.purs b/stbx-core/src/Statebox/Core/WiringTree.purs index d7fdbfe5..9edac66b 100644 --- a/stbx-core/src/Statebox/Core/WiringTree.purs +++ b/stbx-core/src/Statebox/Core/WiringTree.purs @@ -10,7 +10,7 @@ import Data.Tuple.Nested ((/\)) import Data.ArrayMultiset (ArrayMultiset) import Data.Petrinet.Representation.NLL (ErrNetEncoding, TransitionF', fromNLL) -import Statebox.Core.Execution (Path) +import Statebox.Core.Transition (Glued(..), Transition, buildTokens, isInitial, isFinal) import Statebox.Core.Types (Diagram, Net, PID, TID, Wiring) data WiringTree @@ -22,28 +22,6 @@ data WiringTree fromWiring :: Wiring -> Maybe WiringTree fromWiring wiring = Net <$> head wiring.nets -type Transition = - { path :: Path - , transition :: TID - , name :: String - } - -data Glued a - = Untouched a - | Initial a - | Final a - | Glued a a - -isInitial :: ∀ a. Glued a -> Boolean -isInitial = case _ of - Initial a -> true - _ -> false - -isFinal :: ∀ a. Glued a -> Boolean -isFinal = case _ of - Final a -> true - _ -> false - data LinearizationError = DiagramNotYetAllowed | NLLDecodingFailed ErrNetEncoding @@ -65,11 +43,11 @@ linearizeTransitionsAndNames transitions names = sortInitialFinal $ lift3 buildGluedTransition (range 0 (length transitions - 1)) transitions names buildGluedTransition :: TID -> TransitionF' PID -> String -> Glued Transition -buildGluedTransition tId (inputs /\ outputs) name = - case (inputs /\ outputs) of - ([] /\ _ ) -> Initial { name: name, path: [0, 0, 0], transition: tId } -- the path is [0, 0, 0] because we consider a trivial diagram to be there - (_ /\ [] ) -> Final { name: name, path: [0, 0, 0], transition: tId } - (inp /\ out) -> Untouched { name: name, path: [0, 0, 0], transition: tId } +buildGluedTransition tId (pre /\ post) name = + case (pre /\ post) of + ([] /\ _ ) -> Initial { name: name, path: [0, 0, 0], transition: tId, tokens: buildTokens pre post } -- the path is [0, 0, 0] because we consider a trivial diagram to be there + (_ /\ [] ) -> Final { name: name, path: [0, 0, 0], transition: tId, tokens: buildTokens pre post } + (inp /\ out) -> Untouched { name: name, path: [0, 0, 0], transition: tId, tokens: buildTokens pre post } -- | We use this custom function instead of `sortBy` because that does not guarantee -- | the order of equal elements to be preserved. diff --git a/stbx-protocol/spago.dhall b/stbx-protocol/spago.dhall index bfcb21bb..a1bbeec0 100644 --- a/stbx-protocol/spago.dhall +++ b/stbx-protocol/spago.dhall @@ -3,8 +3,10 @@ , name = "stbx-protocol" , dependencies = - [ "stbx-core" + [ "halogen-petrinet-editor" + , "stbx-core" , "stbx-tx-store" + , "studio-common" ] , packages = ./../packages.dhall