val is_breaking_armada_action (pc_breaking: (pc_t -> GTot bool)) (action: Armada.Action.t)
    : GTot bool
val is_breaking_armada_action (pc_breaking: (pc_t -> GTot bool)) (action: Armada.Action.t)
    : GTot bool
let is_breaking_armada_action (pc_breaking: pc_t -> GTot bool) (action: Armada.Action.t) : GTot bool =
    not action.ok
  || is_breaking_optional_pc pc_breaking action.program_statement.end_pc
  || (match action.program_statement.statement with
     | AssertFalseStatement _
     | TerminateProcessStatement _
     | TerminateThreadStatement _
     | MethodCallStatement _ _ _ _ _ true -> true
     | _ -> false)
module Strategies.RegularToAtomic.Armada.Helper

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement.Status
open Strategies.Atomic
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.Behavior
open Util.List
open Util.Nth

let is_breaking_optional_pc
  (pc_breaking: pc_t -> GTot bool)
  (optional_pc: option pc_t)
  : GTot bool =
  match optional_pc with
  | Some pc -> pc_breaking pc
  | None -> true

let pc_breaking_correct_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
     is_breaking_optional_pc pc_breaking ps.start_pc = ps.starts_atomic_block
  && is_breaking_optional_pc pc_breaking ps.end_pc = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (is_breaking_optional_pc pc_breaking ps.start_pc))

let pc_breaking_correct
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (pc_breaking_correct_specific pc_breaking) lprog.program_statements

let created_threads_initially_breaking_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
  match ps.statement with
  | CreateThreadStatement _ initial_pc _ _ _ _ _ -> pc_breaking initial_pc
  | _ -> true

let created_threads_initially_breaking
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (created_threads_initially_breaking_specific pc_breaking) lprog.program_statements

let actions_starting_at_pc_correct_specific
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  (action: Armada.Action.t)
  : GTot ubool =
  contains_ubool action (actions_starting_at_pc action.program_statement.start_pc)

let actions_starting_at_pc_correct
  (lprog: Armada.Program.t)
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  : GTot ubool =
  for_all_ubool (actions_starting_at_pc_correct_specific actions_starting_at_pc) (all_actions lprog.program_statements)

let starting_successors_match_path_infos_specific
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
    successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == [successor.action]

let starting_successors_match_path_infos
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool
    (starting_successors_match_path_infos_specific starting_successors atomic_path_infos)
    starting_successors

let path_successor_matches_path_info
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
     successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == append atomic_path_info.path [successor.action]

let path_successors_match_path_infos_specific
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot ubool =
  for_all_ubool (path_successor_matches_path_info atomic_path_infos atomic_path_info) atomic_path_info.successors

let path_successors_match_path_infos
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (path_successors_match_path_infos_specific atomic_path_infos) atomic_path_infos
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.Status.fsti.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.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.Helper.fst
pc_breaking: (_: Armada.Base.pc_t -> Prims.GTot Prims.bool) -> action: Armada.Action.t
  -> Prims.GTot Prims.bool
Armada.Base.pc_t Prims.bool Armada.Action.t Prims.op_BarBar Prims.op_Negation Armada.Action.__proj__Mkt__item__ok Strategies.RegularToAtomic.Armada.Helper.is_breaking_optional_pc Armada.Action.__proj__Mkprogram_statement_t__item__end_pc Armada.Action.__proj__Mkt__item__program_statement Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Expression.expression_t Armada.Base.method_id_t Prims.list Armada.Base.var_id_t Armada.Init.initializer_t Armada.Statement.t
let is_breaking_armada_action (pc_breaking: (pc_t -> GTot bool)) (action: Armada.Action.t)
    : GTot bool =
  
not action.ok || is_breaking_optional_pc pc_breaking action.program_statement.end_pc ||
(match action.program_statement.statement with
  | AssertFalseStatement _
  | TerminateProcessStatement _
  | TerminateThreadStatement _
  | MethodCallStatement _ _ _ _ _ true -> true
  | _ -> false)