val all_actions (program_statements: list program_statement_t) : list Armada.Action.t
val all_actions (program_statements: list program_statement_t) : list Armada.Action.t
let rec all_actions (program_statements: list program_statement_t) : list Armada.Action.t =
  match program_statements with
  | [] -> []
  | first_program_statement :: remaining_program_statements ->
      { ok = true; program_statement = first_program_statement } ::
      { ok = false; program_statement = first_program_statement } ::
      all_actions remaining_program_statements
module Strategies.Semantics.Armada

open Armada.Action
open Armada.Base
open Armada.Step
open Armada.Program
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Semantics
open Util.Behavior

let armada_step_to_action (step: Armada.Step.t) : Armada.Action.t =
  step.action

let armada_semantics : semantics_t = {
  actor_t = tid_t;
  state_t = Armada.State.t;
  action_t = Armada.Action.t;
  step_t = Armada.Step.t;
  step_to_action_f = armada_step_to_action;
  step_computation_f = Armada.Transition.step_computation;
}
/
Util.Behavior.fst.checked Strategies.Semantics.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Semantics.Armada.fsti
program_statements: Prims.list Armada.Action.program_statement_t -> Prims.list Armada.Action.t
Prims.list Armada.Action.program_statement_t Prims.Nil Armada.Action.t Prims.Cons Armada.Action.Mkt Strategies.Semantics.Armada.all_actions
let rec all_actions (program_statements: list program_statement_t) : list Armada.Action.t =
  
match program_statements with
| [] -> []
| first_program_statement :: remaining_program_statements ->
  { ok = true; program_statement = first_program_statement } ::
  { ok = false; program_statement = first_program_statement } ::
  all_actions remaining_program_statements