val action_breaks (is_breaking_pc: (pc_t -> GTot bool)) (action: Armada.Action.t) : GTot bool
val action_breaks (is_breaking_pc: (pc_t -> GTot bool)) (action: Armada.Action.t) : GTot bool
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)
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
/
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 Prims.op_BarBar Prims.op_Negation Armada.Action.__proj__Mkt__item__ok Strategies.ArmadaStatement.ThreadState.program_statement_to_ending_thread_state Armada.Action.__proj__Mkt__item__program_statement Armada.Thread.thread_status_t Armada.State.stop_reason_t
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)