[#328] [stbx-protocol] implement transition firing

Author: marcosh

stbx-protocol/src/Statebox/Protocol.purs

@@ -1,15 +1,15 @@
 module Statebox.Protocol where
 
 import Prelude
-import Data.Either (Either(..))
+import Data.Either (Either(..), either)
 import Data.Either.Nested (type (\/))
 import Data.Lens ((^?))
 import Data.Maybe (Maybe(..), maybe)
 
+import Data.Petrinet.Representation.Marking (emptyMarking)
 import Statebox.Core.Lenses (_firingExecution)
-
 import Statebox.Core.Transaction (FiringTx, HashStr, HashTx, InitialTx, TxId, TxSum(..), WiringTx, evalTxSum, isInitialTx, isUberRootHash)
--- import Statebox.Protocol.Fire (fire)
+import Statebox.Protocol.Fire (fire)
 import Statebox.Protocol.Store (getTransaction, putTransaction, getExecutionState, updateExecutionState) as Store
 import Statebox.Protocol.Store (StoreActions)
 
@@ -20,25 +20,37 @@ data ProcessError
   = NoUberRoot
 
   -- | The previous transaction of a root (initial) transaction should be an über-root.
-  | InitialPreviousShouldBeUberRoot             TxId
+  | InitialPreviousShouldBeUberRoot                  TxId
 
   -- | The previous transaction of a `Wiring` transaction should be a root (initial) transaction.
-  | WiringPreviousShouldBeInitial               TxId
+  | WiringPreviousShouldBeInitial                    TxId
 
   -- | If an execution already exists, we cannot store it again.
-  | FiringInitialShouldBeCreatedOnlyOnce        TxId
+  | FiringInitialShouldBeCreatedOnlyOnce             TxId
 
   -- | The previous transaction of an initial transaction ('execution transaction') should exist.
-  | FiringInitialShouldHavePrevious             TxId
+  | FiringInitialShouldHavePrevious                  TxId
 
   -- | The previous transaction of an initial transaction ('execution transaction') should be a `Wiring`.
-  | FiringInitialPreviousShouldBeWiring         TxId
+  | FiringInitialPreviousShouldBeWiring              TxId
+
+  -- | The first transition fired should be initial.
+  | FiringInitialTransitionShouldBeInitial           TxId
 
   -- | A normal firing should refer to an existing execution.
-  | FiringNormalShouldHaveExistingExecution     TxId ExecutionId
+  | FiringNormalShouldHaveExistingExecution          TxId ExecutionId
 
   -- | The previous transaction of a normal firing should match the current execution state.
-  | FiringNormalPreviousShouldMatchCurrentState TxId ExecutionId
+  | FiringNormalPreviousShouldMatchCurrentState      TxId ExecutionId
+
+  -- | The execution of a firing should refer to an existing wiring.
+  | FiringNormalExecutionShouldPointToExistingWiring TxId ExecutionId
+
+  -- | The wiring of the execution of a normal firing should be a `Wiring`.
+  | FiringNormalExecutionWiringShouldBeAWiring       TxId ExecutionId
+
+  -- | The fired transition should be enabled.
+  | FiringNormalTransitionShouldBeEnabled            TxId ExecutionId
 
 processTxSum :: HashTx -> StoreActions (ProcessError \/ Unit)
 processTxSum hashTx = case hashTx.tx of
@@ -95,16 +107,19 @@ processInitialFiringTx hash firingTx = do
         -- previous not found
         Nothing       -> pure $ Left $ FiringInitialShouldHavePrevious hash
         -- previous found
-        Just previous -> do
+        Just previous ->
           evalTxSum
             (const $ pure $ Left $ FiringInitialPreviousShouldBeWiring hash)
             (const $ pure $ Left $ FiringInitialPreviousShouldBeWiring hash)
-            (\wiringTx -> map Right $ do
-              -- let firedTransition = fire firingTx
-              Store.putTransaction hash $ FiringTxInj firingTx
-              Store.updateExecutionState hash $ { lastFiring: hash
-                                                , wiring: firingTx.previous
-                                                }
+            (\wiringTx -> either
+              (const $ pure $ Left $ FiringInitialTransitionShouldBeInitial hash)
+              (\newMarking -> map Right $ do
+                Store.putTransaction hash $ FiringTxInj firingTx
+                Store.updateExecutionState hash $ { lastFiring: hash
+                                                  , wiring: firingTx.previous
+                                                  , marking: newMarking
+                                                  })
+              (fire wiringTx.wiring firingTx.firing emptyMarking)
             )
             (const $ pure $ Left $ FiringInitialPreviousShouldBeWiring hash)
             previous
@@ -119,10 +134,23 @@ processNormalFiringTx hash firingTx executionHash = do
     Just execution -> do
       -- check if the previous transaction corresponds to the current state of the execution
       if firingTx.previous == execution.lastFiring
-      then map Right $ do
-        -- fire transition
-        Store.putTransaction hash $ FiringTxInj firingTx
-        Store.updateExecutionState executionHash { lastFiring: hash
-                                                 , wiring: execution.wiring
-                                                 }
+      then do
+        maybeWiring <- Store.getTransaction execution.wiring
+        case maybeWiring of
+          Nothing          -> pure $ Left $ FiringNormalExecutionShouldPointToExistingWiring hash executionHash
+          Just transaction ->
+            evalTxSum
+              (const $ pure $ Left $ FiringNormalExecutionWiringShouldBeAWiring hash executionHash)
+              (const $ pure $ Left $ FiringNormalExecutionWiringShouldBeAWiring hash executionHash)
+              (\wiringTx -> either
+                (const $ pure $ Left $ FiringNormalTransitionShouldBeEnabled hash executionHash)
+                (\newMarking -> map Right $ do
+                  Store.putTransaction hash $ FiringTxInj firingTx
+                  Store.updateExecutionState executionHash { lastFiring: hash
+                                                          , wiring: execution.wiring
+                                                          , marking: newMarking
+                                                          })
+                (fire wiringTx.wiring firingTx.firing execution.marking))
+              (const $ pure $ Left $ FiringNormalExecutionWiringShouldBeAWiring hash executionHash)
+              transaction
       else pure $ Left $ FiringNormalPreviousShouldMatchCurrentState hash executionHash

stbx-protocol/src/Statebox/Protocol/ExecutionState.purs

@@ -1,8 +1,10 @@
 module Statebox.Protocol.ExecutionState where
 
 import Statebox.Core.Transaction (TxId)
+import View.Petrinet.Model (Marking)
 
 type ExecutionState =
   { lastFiring :: TxId
   , wiring     :: TxId
+  , marking    :: Marking
   }

stbx-protocol/src/Statebox/Protocol/Fire.purs

@@ -1,6 +1,44 @@
 module Statebox.Protocol.Fire where
 
-import Statebox.Core.Transaction (FiringTx)
+import Prelude
+import Data.Array (index)
+import Data.Either (Either(..), either)
+import Data.Either.Nested (type (\/))
+import Data.Maybe (maybe)
+import Data.NonEmpty (head)
 
--- fire :: ∀ a . FiringTx -> a
--- fire = ?fire
+import Data.Petrinet.Representation.Dict (fireAtMarking)
+import Statebox.Core.Transition (gluedTokens)
+import Statebox.Core.Types (Firing, Wiring)
+import Statebox.Core.WiringTree (LinearizationError, fromWiring, linearize)
+import View.Petrinet.Model (Marking)
+
+data FiringError
+
+  -- | The wiring does not describe a valid wiring tree.
+  = FireInvalidWiringTree
+
+  -- | The linerization of the wiring tree failed with a LinerizationError
+  | FireLinerizationError LinearizationError
+
+  -- | The path of the firing describing
+  | FireTransitionIndexOutOfBounds
+
+  -- | The selected transition is not enabled
+  | FireTransitionNotEnabled
+
+fire :: Wiring -> Firing -> Marking -> FiringError \/ Marking
+fire wiring firing marking = maybe
+  (Left FireInvalidWiringTree)
+  (\wiringTree ->
+    either
+      (Left <<< FireLinerizationError)
+      (\gluedTransitions ->
+        let transitionIndex = head firing.path
+        in maybe
+          (Left FireTransitionIndexOutOfBounds)
+          (\gluedTransition ->
+            Right $ fireAtMarking marking $ gluedTokens gluedTransition)
+          (index gluedTransitions transitionIndex))
+      (linearize wiringTree))
+  (fromWiring wiring)