val actions_end_with_all_threads_breaking
      (is_breaking_pc: (pc_t -> GTot bool))
      (actions: list Armada.Action.t)
    : GTot bool
val actions_end_with_all_threads_breaking
      (is_breaking_pc: (pc_t -> GTot bool))
      (actions: list Armada.Action.t)
    : GTot bool
let rec actions_end_with_all_threads_breaking
  (is_breaking_pc: pc_t -> GTot bool)
  (actions: list Armada.Action.t)
  : GTot bool =
  match actions with
  | [] -> false
  | [last_action] ->
         action_only_creates_breaking_threads is_breaking_pc last_action
      && action_breaks is_breaking_pc last_action
  | first_action :: remaining_actions ->
         action_only_creates_breaking_threads is_breaking_pc first_action
      && actions_end_with_all_threads_breaking is_breaking_pc remaining_actions
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)

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
/
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) ->
    actions: Prims.list Armada.Action.t
  -> Prims.GTot Prims.bool
Armada.Base.pc_t Prims.bool Prims.list Armada.Action.t Prims.op_AmpAmp Strategies.Breaking.action_only_creates_breaking_threads Strategies.Breaking.action_breaks Strategies.Breaking.actions_end_with_all_threads_breaking
let rec actions_end_with_all_threads_breaking
      (is_breaking_pc: (pc_t -> GTot bool))
      (actions: list Armada.Action.t)
    : GTot bool =
  
match actions with
| [] -> false
| [last_action] ->
  action_only_creates_breaking_threads is_breaking_pc last_action &&
  action_breaks is_breaking_pc last_action
| first_action :: remaining_actions ->
  action_only_creates_breaking_threads is_breaking_pc first_action &&
  actions_end_with_all_threads_breaking is_breaking_pc remaining_actions