necoherence/typed_mapping

Types

AcyclicWitness

pub type AcyclicWitness {
  AcyclicWitness(
    explored_markings: List(Marking),
    steps: Int,
    frontier: List(Marking),
  )
}

Constructors

AcyclicWitness(
  explored_markings: List(Marking),
  steps: Int,
  frontier: List(Marking),
)

ClosureWitness

The finite closure a bounded search actually explored, proving no marking in it satisfies the goal.

pub type ClosureWitness {
  ClosureWitness(
    explored_markings: List(Marking),
    steps: Int,
    frontier: List(Marking),
  )
}

Constructors

ClosureWitness(
  explored_markings: List(Marking),
  steps: Int,
  frontier: List(Marking),
)

ColoredToken

A colored token: the resource it belongs to, its declared position, its revision, and its kind.

pub type ColoredToken {
  ColoredToken(
    target: String,
    index: Int,
    revision: Int,
    kind: TokenKind,
  )
}

Constructors

ColoredToken(
  target: String,
  index: Int,
  revision: Int,
  kind: TokenKind,
)

CycleWitness

pub type CycleWitness {
  CycleWitness(
    prefix_path: List(String),
    cycle_path: List(String),
    cycle_start: Marking,
    cycle_end: Marking,
    measure_decreasing: Bool,
  )
}

Constructors

CycleWitness(
  prefix_path: List(String),
  cycle_path: List(String),
  cycle_start: Marking,
  cycle_end: Marking,
  measure_decreasing: Bool,
)

The closed result of deciding whether a marking is a deadlock: Deadlocked carries the marking observed with nothing enabled, NotDeadlocked carries the set of enabled transitions, and DeadlockUnknown and DeadlockInvalid carry why the bounded search could not settle it or why the declared mapping is invalid.

pub type DeadlockResult {
  Deadlocked(DeadlockWitness)
  NotDeadlocked(EnabledSet)
  DeadlockUnknown(UnknownReason)
  DeadlockInvalid(InvalidReason)
}

Constructors

```
Deadlocked(DeadlockWitness)
```
```
NotDeadlocked(EnabledSet)
```
```
DeadlockUnknown(UnknownReason)
```
```
DeadlockInvalid(InvalidReason)
```

DeadlockWitness

The marking a deadlock was observed at.

pub type DeadlockWitness {
  DeadlockWitness(marking: Marking)
}

Constructors

```
DeadlockWitness(marking: Marking)
```

DeclarationGraph

The dependency graph over declared places and transitions.

pub type DeclarationGraph {
  DeclarationGraph(
    places: List(String),
    transitions: List(String),
    edges: List(#(String, String)),
    revision: Int,
  )
}

Constructors

DeclarationGraph(
  places: List(String),
  transitions: List(String),
  edges: List(#(String, String)),
  revision: Int,
)

DomainBound

The finite domain and search bound: how many binding-carrying transitions and how many search steps the solver may explore.

pub type DomainBound {
  DomainBound(
    target_identity: String,
    index: Int,
    revision: Int,
    max_bindings: Int,
    max_search_steps: Int,
  )
}

Constructors

DomainBound(
  target_identity: String,
  index: Int,
  revision: Int,
  max_bindings: Int,
  max_search_steps: Int,
)

EnabledResult

The closed result of derive_enabled_set and derive_enabled.

pub type EnabledResult {
  Enabled(EnabledSet)
  EnabledInvalid(InvalidReason)
}

Constructors

```
Enabled(EnabledSet)
```
```
EnabledInvalid(InvalidReason)
```

EnabledSet

The finite set of binding-carrying transitions enabled by a marking.

pub type EnabledSet {
  EnabledSet(enabled: List(EnabledTransition))
}

Constructors

EnabledSet(enabled: List(EnabledTransition))

EnabledTransition

One enabled transition together with the bindings it was enabled by.

pub type EnabledTransition {
  EnabledTransition(
    transition_id: String,
    bindings: List(InputBinding),
  )
}

Constructors

EnabledTransition(
  transition_id: String,
  bindings: List(InputBinding),
)

GoalPredicate

A finite, decidable predicate over a marking: which place must carry how many tokens, or which exact token, combined by GoalAnd/GoalOr/ GoalNot.

pub type GoalPredicate {
  PlaceHasAtLeast(place: String, count: Int)
  PlaceHasToken(
    place: String,
    target: String,
    index: Int,
    revision: Int,
  )
  GoalAnd(a: GoalPredicate, b: GoalPredicate)
  GoalOr(a: GoalPredicate, b: GoalPredicate)
  GoalNot(a: GoalPredicate)
}

Constructors

PlaceHasAtLeast(place: String, count: Int)

PlaceHasToken(
  place: String,
  target: String,
  index: Int,
  revision: Int,
)

GoalAnd(a: GoalPredicate, b: GoalPredicate)

GoalOr(a: GoalPredicate, b: GoalPredicate)

```
GoalNot(a: GoalPredicate)
```

InputBinding

One declared input binding for one transition: the place it reads from, the type and identity it requires, and the revision every matched token must carry.

pub type InputBinding {
  InputBinding(
    transition_id: String,
    name: String,
    place: String,
    token_type: String,
    identity: String,
    provenance: String,
    multiplicity: Int,
    mode: BindingMode,
    required_revision: Int,
  )
}

Constructors

InputBinding(
  transition_id: String,
  name: String,
  place: String,
  token_type: String,
  identity: String,
  provenance: String,
  multiplicity: Int,
  mode: BindingMode,
  required_revision: Int,
)

InvalidReason

Why a declared typed mapping is invalid.

pub type InvalidReason {
  UnknownPlace(place: String)
  UnknownTransition(transition_id: String)
  UnknownInputPlace(transition_id: String, place: String)
  MissingInputBinding(transition_id: String, place: String)
  DuplicateTransitionIdentity(identity: String)
  TypeMismatch(place: String, expected: String, actual: String)
  MultiplicityMismatch(
    transition_id: String,
    name: String,
    expected: Int,
    actual: Int,
  )
  RevisionMismatch(
    transition_id: String,
    name: String,
    expected: Int,
    actual: Int,
  )
  IdentityMismatch(transition_id: String, name: String)
  DependencyMismatch(transition_id: String, place: String)
}

Constructors

```
UnknownPlace(place: String)
```

UnknownTransition(transition_id: String)

UnknownInputPlace(transition_id: String, place: String)

MissingInputBinding(transition_id: String, place: String)

DuplicateTransitionIdentity(identity: String)

TypeMismatch(place: String, expected: String, actual: String)

MultiplicityMismatch(
  transition_id: String,
  name: String,
  expected: Int,
  actual: Int,
)

RevisionMismatch(
  transition_id: String,
  name: String,
  expected: Int,
  actual: Int,
)

IdentityMismatch(transition_id: String, name: String)

DependencyMismatch(transition_id: String, place: String)

Marking

A marking: for each place, the multiset (as a list) of tokens it carries.

pub type Marking {
  Marking(places: List(#(String, List(ColoredToken))))
}

Constructors

Marking(places: List(#(String, List(ColoredToken))))

ReachabilityResult

The closed result of deciding whether a marking satisfying the goal is reachable: Reachable carries the firing sequence that reaches one, Unreachable carries the explored closure containing none, and ReachabilityUnknown and ReachabilityInvalid carry why the bounded search could not settle it or why the declared mapping is invalid.

pub type ReachabilityResult {
  Reachable(ReachabilityWitness)
  Unreachable(ClosureWitness)
  ReachabilityUnknown(UnknownReason)
  ReachabilityInvalid(InvalidReason)
}

Constructors

```
Reachable(ReachabilityWitness)
```
```
Unreachable(ClosureWitness)
```
```
ReachabilityUnknown(UnknownReason)
```
```
ReachabilityInvalid(InvalidReason)
```

ReachabilityWitness

The firing sequence and marking that satisfied a goal.

pub type ReachabilityWitness {
  ReachabilityWitness(path: List(String), final_marking: Marking)
}

Constructors

ReachabilityWitness(path: List(String), final_marking: Marking)

SolverFailure

A violated host contract or an impossible implementation invariant; never a declaration mismatch, which is always the closed invalid result.

pub type SolverFailure {
  ContractViolation(message: String)
  InternalInvariantViolation(message: String)
}

Constructors

```
ContractViolation(message: String)
```

InternalInvariantViolation(message: String)

SolverInput

The complete, closed input to every solver operation.

pub type SolverInput {
  SolverInput(
    places: List(TypedPlace),
    transitions: List(TypedTransition),
    bindings: List(InputBinding),
    goal: GoalPredicate,
    graph: DeclarationGraph,
    marking: Marking,
    bound: DomainBound,
  )
}

Constructors

SolverInput(
  places: List(TypedPlace),
  transitions: List(TypedTransition),
  bindings: List(InputBinding),
  goal: GoalPredicate,
  graph: DeclarationGraph,
  marking: Marking,
  bound: DomainBound,
)

TokenKind

What role a token plays at the point it is carried.

pub type TokenKind {
  TokenInput
  TokenOutput
  TokenFailure
  TokenEffect
  TokenObservation
  TokenAccepted
}

Constructors

```
TokenInput
```
```
TokenOutput
```
```
TokenFailure
```
```
TokenEffect
```
```
TokenObservation
```
```
TokenAccepted
```

TypedPlace

A declared typed place: its identity, the token type it carries, and its revision.

pub type TypedPlace {
  TypedPlace(identity: String, token_type: String, revision: Int)
}

Constructors

TypedPlace(identity: String, token_type: String, revision: Int)

TypedTransition

A declared typed transition: its identity, declared input, output and failure places, and its revision.

pub type TypedTransition {
  TypedTransition(
    identity: String,
    input_places: List(String),
    output_places: List(String),
    failure_places: List(String),
    revision: Int,
  )
}

Constructors

TypedTransition(
  identity: String,
  input_places: List(String),
  output_places: List(String),
  failure_places: List(String),
  revision: Int,
)

UnknownReason

Why a bounded search could not settle a result.

pub type UnknownReason {
  BindingBoundExhausted(limit: Int)
  SearchStepBoundExhausted(limit: Int)
}

Constructors

```
BindingBoundExhausted(limit: Int)
```
```
SearchStepBoundExhausted(limit: Int)
```

WellFoundednessResult

The closed result of deciding whether the firing relation is well-founded: WellFounded carries the acyclic closure explored, NotWellFounded carries a witnessing cycle, and WellFoundednessUnknown and WellFoundednessInvalid carry why the bounded search could not settle it or why the declared mapping is invalid.

pub type WellFoundednessResult {
  WellFounded(AcyclicWitness)
  NotWellFounded(CycleWitness)
  WellFoundednessUnknown(UnknownReason)
  WellFoundednessInvalid(InvalidReason)
}

Constructors

```
WellFounded(AcyclicWitness)
```
```
NotWellFounded(CycleWitness)
```
```
WellFoundednessUnknown(UnknownReason)
```
```
WellFoundednessInvalid(InvalidReason)
```

Values

apply_branch_at

pub fn apply_branch_at(
  marking: Marking,
  t: TypedTransition,
  bindings: List(InputBinding),
) -> Marking

Atomically apply one declared result branch: consume bindings remove their tokens, read bindings retain theirs and every declared output place gains the produced token. Nothing is promoted to an observation.

binding_bound_exceeded

pub fn binding_bound_exceeded(input: SolverInput) -> Bool

Whether binding enumeration exceeds the declared bound max_bindings; operations then report Unknown(BindingBoundExhausted(_)).

bindings_for

pub fn bindings_for(
  input: SolverInput,
  transition_id: String,
) -> List(InputBinding)

The declared input bindings of one transition.

check_closure_required_for_unreachable

pub fn check_closure_required_for_unreachable(
  closure_complete: Bool,
  reported_unreachable: Bool,
) -> Bool

Unreachable may only be reported together with a fully-explored (non-bound-exhausted) closure.

check_deadlock_goal_separation

pub fn check_deadlock_goal_separation(
  goal_holds: Bool,
  deadlocked: Bool,
) -> Bool

Deadlock and goal satisfaction never hold at the same marking.

check_read_consume_atomicity

pub fn check_read_consume_atomicity(
  before: List(ColoredToken),
  consumed: List(ColoredToken),
  retained: List(ColoredToken),
) -> Bool

Multiset atomicity of consumption: retained count equals prior count minus consumed count per token identity. Unselected structurally equal duplicates remain.

check_token_color_preserved

pub fn check_token_color_preserved(
  before: List(ColoredToken),
  after: List(ColoredToken),
) -> Bool

Every token surviving consumption at a place was already present there; consumption never invents or mutates a token’s color.

derive_enabled

pub fn derive_enabled(
  input: SolverInput,
) -> Result(EnabledResult, SolverFailure)

Derive the finite set of binding-carrying transitions enabled by input.marking, after validating the declaration. The function is pure and total, with no effects; host failures report on the Result error channel.

derive_enabled_set

pub fn derive_enabled_set(input: SolverInput) -> EnabledResult

Derive the finite set of binding-carrying transitions enabled by input.marking, after validating the declaration.

eval_goal

pub fn eval_goal(marking: Marking, goal: GoalPredicate) -> Bool

Evaluate a goal predicate against a marking.

tokens_at

pub fn tokens_at(
  marking: Marking,
  place: String,
) -> List(ColoredToken)

The tokens a marking carries at one place; a place absent from the marking carries none.

transition_enabled_at

pub fn transition_enabled_at(
  bindings: List(InputBinding),
  marking: Marking,
) -> Bool

Whether every one of a transition’s declared bindings is satisfied at a marking.

validate

pub fn validate(input: SolverInput) -> Result(Nil, InvalidReason)