val step_computation
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : GTot (option Armada.State.t)
val step_computation
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : GTot (option Armada.State.t)
let step_computation
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (step: Armada.Step.t)
  (s: Armada.State.t)
  : GTot (option Armada.State.t) =
  action_computation actor starts_atomic_block ends_atomic_block step.nd step.action s
module Armada.Transition

open Armada.Action
open Armada.Base
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Threads
open Armada.Type
open Spec.List
open Spec.Ubool

noeq type t = {
  actor: tid_t;
  steps: list Armada.Step.t;
}
/
Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Armada.Transition.fst

    actor: Armada.Base.tid_t ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    step: Armada.Step.t ->
    s: Armada.State.t
  -> Prims.GTot (FStar.Pervasives.Native.option Armada.State.t)
Armada.Base.tid_t Prims.bool Armada.Step.t Armada.State.t Armada.Action.action_computation Armada.Step.__proj__Mkt__item__nd Armada.Step.__proj__Mkt__item__action FStar.Pervasives.Native.option
let step_computation
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : GTot (option Armada.State.t) =
  
action_computation actor starts_atomic_block ends_atomic_block step.nd step.action s