val armada_created_threads_initially_breaking_specific
      (pc_index_breaking: array_t bool)
      (pc_indices: statement_pc_indices_t)
    : GTot bool
val armada_created_threads_initially_breaking_specific
      (pc_index_breaking: array_t bool)
      (pc_indices: statement_pc_indices_t)
    : GTot bool
let armada_created_threads_initially_breaking_specific
  (pc_index_breaking: array_t bool)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  armada_is_breaking_optional_pc pc_index_breaking pc_indices.create_thread_initial_pc_index
module Strategies.RegularToAtomic.Armada

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range

type armada_successor_info_t = {
  action_index: nat;
  path_index: nat;
}

type armada_atomic_path_info_t = {
  path: list nat;
  atomic_action_index_or_successors: either nat (list armada_successor_info_t);
}

let armada_is_breaking_optional_pc
  (pc_index_breaking: array_t bool)
  (optional_pc_index: option nat)
  : GTot bool =
  match optional_pc_index with
  | Some pc_index -> if pc_index < array_len pc_index_breaking then array_index pc_index_breaking pc_index else true
  | None -> true

let armada_pc_breaking_correct_specific
  (pc_index_breaking: array_t bool)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  let ps = action.program_statement in
     armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index = ps.starts_atomic_block
  && armada_is_breaking_optional_pc pc_index_breaking pc_indices.end_pc_index = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index))

let armada_pc_breaking_correct
  (actions_array: array_t Armada.Action.t)
  (pc_indices_array: array_t statement_pc_indices_t)
  (pc_index_breaking: array_t bool)
  : GTot bool =
  arrays_correspond (armada_pc_breaking_correct_specific pc_index_breaking) actions_array pc_indices_array
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.fsti

    pc_index_breaking: Util.ImmutableArray.array_t Prims.bool ->
    pc_indices: Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Prims.bool Strategies.PCIndices.statement_pc_indices_t Strategies.RegularToAtomic.Armada.armada_is_breaking_optional_pc Strategies.PCIndices.__proj__Mkstatement_pc_indices_t__item__create_thread_initial_pc_index
let armada_created_threads_initially_breaking_specific
      (pc_index_breaking: array_t bool)
      (pc_indices: statement_pc_indices_t)
    : GTot bool =
  
armada_is_breaking_optional_pc pc_index_breaking pc_indices.create_thread_initial_pc_index