val action_only_creates_breaking_threads
      (is_breaking_pc: (pc_t -> GTot bool))
      (action: Armada.Action.t)
    : GTot bool
val action_only_creates_breaking_threads
      (is_breaking_pc: (pc_t -> GTot bool))
      (action: Armada.Action.t)
    : GTot bool
let action_only_creates_breaking_threads
  (is_breaking_pc: pc_t -> GTot bool)
  (action: Armada.Action.t)
  : GTot bool =
  match action.program_statement.statement with
  | CreateThreadStatement _ initial_pc _ _ _ _ _ -> is_breaking_pc initial_pc
  | _ -> true
module Strategies.Breaking

open Armada.Action
open Armada.Base
open Armada.Statement
open Armada.Transition
open Spec.List
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.List

let action_breaks
  (is_breaking_pc: pc_t -> GTot bool)
  (action: Armada.Action.t)
  : GTot bool =
    (not action.ok)
  || (match program_statement_to_ending_thread_state action.program_statement with
     | ThreadStateRunning -> false
     | ThreadStateAtPC pc -> is_breaking_pc pc
     | ThreadStateNotRunning status -> true
     | ThreadStateProcessStopped stop_reason -> true)
/
Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Transition.fst.checked Armada.Statement.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Breaking.fst
is_breaking_pc: (_: 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 Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Armada.Base.method_id_t FStar.Pervasives.Native.option Armada.Expression.expression_t Prims.list Armada.Base.var_id_t Armada.Init.initializer_t Armada.Statement.t
let action_only_creates_breaking_threads
      (is_breaking_pc: (pc_t -> GTot bool))
      (action: Armada.Action.t)
    : GTot bool =
  
match action.program_statement.statement with
| CreateThreadStatement _ initial_pc _ _ _ _ _ -> is_breaking_pc initial_pc
| _ -> true