w.i.p

Author: jonaprieto

docs/everything.juvix.md

@@ -20,7 +20,7 @@ import node_architecture.types.identities;
 import node_architecture.types.messages;
 import node_architecture.types.engine_environment;
 import node_architecture.types.engine_dynamics;
-import node_architecture.types.engine_family;
+import node_architecture.types.engine;
 import node_architecture.types.anoma_environment;
 import node_architecture.types.anoma_message;
 import node_architecture.types;

docs/node_architecture/engines.md

@@ -90,3 +90,5 @@ This establishes a total order of transactions for the [execution engine](./engi
 Proofs from the execution engine allow light clients to read the current state.
 When the execution engine has processed a transaction, it communicates to the [mempool](./engines/mempool.md#mempool) that the transaction can data can be garbage-collected from storage.
 [Read more here.](./engines/execution.md#execution)
+
+Each engine implements a specific `EngineBehaviour` that defines its core dynamics and operational characteristics. The behaviour determines how the engine processes inputs, manages state, and interacts with other components.

docs/node_architecture/engines/index.md

@@ -53,7 +53,7 @@ engine instances will have. For Anoma specifications, the components are:
 
 For the Anoma Specification, engine families are written in Juvix Markdown. All
 necessary types and functions to define these engines can be found in the module
-[[Engine Family Types|engine_family]].
+[[Engine Behaviour Types|engine_family]].
 See [[Engines in Anoma|Tutorials on Writing Engine Families]] for a tutorial on
 how to structure the writing of engine families in Juvix.
 
@@ -73,4 +73,4 @@ families.
 ## Useful Links
 
 - [[Engines in Anoma|Tutorials on Writing Engine Families]]
-- [[Ticker Engine Overview|Example Engine Family]]
+- [[Ticker Engine Overview|Example Engine Behaviour]]

docs/node_architecture/engines/template.juvix.md

@@ -15,22 +15,22 @@ tags:
       import node_architecture.engines.template_overview open public;
       import node_architecture.engines.template_environment open public;
       import node_architecture.engines.template_dynamics open public;
-      import node_architecture.types.engine_family as Anoma;
+      import node_architecture.types.engine_behaviour as Anoma;
     ```
 
 # `Template` engine family type
 
 <!-- --8<-- [start:template-engine-family] -->
 ```juvix
-TemplateEngineFamily :
-  Anoma.EngineFamily
+TemplateEngineBehaviour :
+  Anoma.EngineBehaviour
     TemplateLocalState
     TemplateMailboxState
     TemplateTimerHandle
     TemplateMatchableArgument
     TemplateActionLabel
     TemplatePrecomputation
-  := Anoma.mkEngineFamily@{
+  := Anoma.mkEngineBehaviour@{
     guards := [messageOneGuard];
     action := templateAction;
     conflictSolver := templateConflictSolver;

docs/node_architecture/engines/template_overview.juvix.md

@@ -16,7 +16,7 @@ tags:
     import prelude open;
     ```
 
-# `Template` Engine Family Overview
+# `Template` Engine Behaviour Overview
 
 --8<-- "./docs/node_architecture/engines/template.juvix.md:template-engine-family"
 

docs/node_architecture/engines/ticker.juvix.md

@@ -12,32 +12,53 @@ tags:
     ```juvix
     module node_architecture.engines.ticker;
       import prelude open;
-      import node_architecture.types.engine_family as Anoma;
+      import node_architecture.types.engine_behaviour as E;
 
       import node_architecture.engines.ticker_overview open public;
       import node_architecture.engines.ticker_environment open public;
       import node_architecture.engines.ticker_dynamics open public;
     ```
 
-# Ticker engine family type
+# Ticker engine behaviour
 
-<!-- --8<-- [start:ticker-engine-family] -->
+<!-- --8<-- [start:ticker-engine-behaviour] -->
 ```juvix
-TickerEngineFamily :
-  Anoma.EngineFamily
+TickerEngineBehaviour :
+  E.EngineBehaviour
     TickerLocalState
     TickerMailboxState
     TickerTimerHandle
     TickerMatchableArgument
     TickerActionLabel
     TickerPrecomputation
-  := Anoma.mkEngineFamily@{
+  := E.mkEngineBehaviour@{
     guards := [incrementGuard ; countGuard];
     action := tickerAction;
     conflictSolver := tickerConflictSolver;
   }
   ;
 ```
-<!-- --8<-- [end:ticker-engine-family] -->
+<!-- --8<-- [end:ticker-engine-behaviour] -->
 
 
+```juvix
+TickerEngine : 
+E.Engine   TickerLocalState
+    TickerMailboxState
+    TickerTimerHandle
+    TickerMatchableArgument
+    TickerActionLabel
+    TickerPrecomputation
+ := E.mkEngine@{
+  name := "ticker";
+  behaviour := TickerEngineBehaviour;
+  initEnv := E.mkEngineEnvironment@{
+    name := "ticker";
+    localState := Unit;
+    mailboxCluster := Map.empty;
+    acquaintances := Set.empty;
+    timers := [];
+  };
+};
+
+```

docs/node_architecture/engines/ticker_dynamics.juvix.md

@@ -290,6 +290,6 @@ tickerAction (input : TickerActionInput) : TickerActionEffect
 tickerConflictSolver : Set TickerMatchableArgument -> List (Set TickerMatchableArgument) := \{ _ := [] }
 ```
 
-## `Ticker` Engine Family Summary
+## `Ticker` Engine Behaviour Summary
 
 --8<-- "./docs/node_architecture/engines/ticker.juvix.md:ticker-engine-family"

docs/node_architecture/engines/ticker_overview.juvix.md

@@ -15,7 +15,7 @@ tags:
     module node_architecture.engines.ticker_overview;
     ```
 
-# `Ticker` Engine Family Overview
+# `Ticker` Engine Behaviour Overview
 
 --8<-- "./docs/node_architecture/engines/ticker.juvix.md:ticker-engine-family"
 

docs/node_architecture/types/engine.juvix.md

@@ -0,0 +1,99 @@
+---
+icon: octicons/project-template-24
+search:
+  exclude: false
+tags:
+- engine-behaviour
+- engine-type
+- juvix
+---
+
+??? quote "Juvix imports"
+
+    ```juvix
+    module node_architecture.types.engine;
+    import prelude open;
+    import node_architecture.types.identities open;
+    import node_architecture.types.engine_environment open public;
+    import node_architecture.types.engine_dynamics open public;
+    ```
+
+# Engine
+
+An **engine** is a computational unit with a specific name and behaviour, plus its
+own execution context called the engine environment, which comprises the
+specific state, the mailbox cluster, the acquaintances, and the timers. An
+engine instance is of type `Engine` instantiated with the types for the local
+states, the mailboxes' state, the time handles, the action-label action, and the
+precomputation. We use the following conventions:
+
+- to the type for the local states as `S`,
+- for the mailboxes' state as `M`,
+- for the time handles as `H`,
+- for the action-label as `A`,
+- for the precomputation as `L`, and
+- for the external inputs as `X`.
+
+To define the type for engine instances, we first need to define the type for
+engine behaviours.
+
+## Engine behaviour type
+
+The `EngineBehaviour` type encapsulates the concept of behaviours within Anoma. As
+defined, it clears up that engines are essentially a collection of guarded
+state-transition functions.
+
+```juvix
+type EngineBehaviour (S M H A L X : Type) := mkEngineBehaviour {
+  guards : List (Guard S M H A L X);
+  action : ActionFunction S M H A L X;
+  conflictSolver : Set A -> List (Set A);
+};
+```
+
+!!! info "On the use of `List` for guards in `EngineBehaviour`"
+
+    The `EngineBehaviour` type uses `List` for guards to enable parallel
+    processing. This choice acknowledges that guards can be concurrent or
+    competing, with the latter requiring priority assignment to resolve
+    non-determinism. While guards should form a set, using `List` simplifies the
+    implementation and provides an inherent ordering.
+
+## Engine instance type
+
+An *engine* is a term of type `Engine` instantiated with the types for the local
+states, the mailboxes' state, the time handles, the action-label action, and the
+precomputation. Each engine, not its type, is associated with:
+
+- a specific name (unique across the system),
+- a specific behaviour, and
+- a declaration of its own execution context, that is, the specific state, the
+  mailbox cluster, the acquaintances, and the timers.
+  
+```juvix
+type Engine (S M H A L X : Type) := mkEngine {
+  name : EngineName;
+  family : EngineBehaviour S M H A L X;
+  initEnv : EngineEnvironment S M H;
+};
+```
+
+!!! example "Voting Engine"
+
+    As an example, we could define an engine type for a voting system:
+
+    - `S` could be a record with fields like `votes`, `voters`, and `results`.
+    - The engine-specific message type might be a coproduct of `Vote` and `Result`.
+    - The behaviour of this engine may include guarded actions like:
+        - `storeVote` to store a vote in the local state,
+        - `computeResult` to compute the result of the election, and
+        - `announceResult` to send the result to some other engine instances.
+
+    With each different election or kind of voters, we obtain a new engine instance,
+    while the underlining voting system, the voting engine family, remains the same.
+
+!!! note
+
+    Both the `EngineBehaviour` and `Engine` types are parameterised by several types. When
+    not used in the context of a new engine family declaration, these types can be
+    replaced by the unit type `Unit`.

docs/node_architecture/types/engine_environment.juvix.md

@@ -3,9 +3,9 @@ icon: octicons/project-template-24
 search:
   exclude: false
 tags:
-- Engine-Family
-- Engine-Instances
-- Juvix
+- engine-environment
+- engine-instances
+- juvix
 ---
 
 ??? quote "Juvix imports"
@@ -18,13 +18,13 @@ tags:
     import node_architecture.types.anoma_message as Anoma;
     ```
 
-# Engine family environment type
+# Engine behaviour environment type
 
-The engine family environment encompasses static information for engine
+The engine behaviour environment encompasses static information for engine
 instances in the following categories:
 
 - A global reference, `name`, for the engine instance.
-- Local state whose type is specific to the engine family.
+- Local state whose type is specific to the engine behaviour.
 - Mailbox cluster, which is a map of mailbox IDs to mailboxes.
 - A set of names of acquainted engine instances. It is implicit that the engine
   instance is acquainted with itself, so there is no need to include its own
@@ -44,7 +44,7 @@ types.
 ```juvix
 type EngineEnvironment (S M H : Type) :=
   mkEngineEnvironment {
-      name : EngineName ; -- read-only
+      name : EngineName ; -- read-only and for internal use only
       localState : S;
       mailboxCluster : Map MailboxID (Mailbox M);
       acquaintances : Set EngineName;