val armada_program_to_generic (program: Armada.Program.t) : program_t armada_semantics
val armada_program_to_generic (program: Armada.Program.t) : program_t armada_semantics
let armada_program_to_generic (program: Armada.Program.t) : program_t armada_semantics = {
  init_f = Armada.Program.init_program program;
  actions = all_actions program.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;
}

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

val all_actions_has_all_actions
  (action: Armada.Action.t)
  (program_statements: list program_statement_t)
  : Lemma (contains_ubool action.program_statement program_statements <==>
             (contains_ubool action (all_actions program_statements)))
/
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: Armada.Program.t
  -> Strategies.Semantics.program_t Strategies.Semantics.Armada.armada_semantics
Armada.Program.t Strategies.Semantics.Mkprogram_t Strategies.Semantics.Armada.armada_semantics Armada.Program.init_program Strategies.Semantics.Armada.all_actions Armada.Program.__proj__Mkt__item__program_statements Strategies.Semantics.program_t
let armada_program_to_generic (program: Armada.Program.t) : program_t armada_semantics =
  
{ init_f = Armada.Program.init_program program; actions = all_actions program.program_statements }