val update_thread_pc_in_state (s: Armada.State.t) (tid: tid_t) (opc: option pc_t) : Armada.State.t
val update_thread_pc_in_state (s: Armada.State.t) (tid: tid_t) (opc: option pc_t) : Armada.State.t
let update_thread_pc_in_state (s: Armada.State.t) (tid: tid_t) (opc: option pc_t) : Armada.State.t =
  match opc with
  | Some pc ->
      let thread = s.threads tid in
      let new_thread = { thread with pc = pc; } in
      let new_threads = Spec.Map.upd s.threads tid new_thread in
      { s with threads = new_threads }
  | None -> s
module Armada.Action

open Armada.Base
open Armada.Computation
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Type
open Spec.Logic
open Spec.Map
open Spec.Ubool

noeq type program_statement_t = {
  start_pc: option pc_t;         // if Some `x`, then actor's PC must be at `x` when action begins
  end_pc: option pc_t;           // if end_pc is Some `y`, then actor's PC is changed to `y` by the action;
                                 // if end_pc is None and start_pc is None, then actor's PC is unchanged by the action;
                                 // if end_pc is None and start_pc is Some `x`, then actor is terminated by the action
  starts_atomic_block: bool;     // whether this action starts with the actor yielded
  ends_atomic_block: bool;       // whether this action causes the actor to yield when ok=true
  statement: Armada.Statement.t; // statement to be executed before performing end_pc modification
}

noeq type t = {
  ok: bool;
  program_statement: program_statement_t;
}
/
Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.Logic.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Armada.Action.fst
s: Armada.State.t -> tid: Armada.Base.tid_t -> opc: FStar.Pervasives.Native.option Armada.Base.pc_t
  -> Armada.State.t
Armada.State.t Armada.Base.tid_t FStar.Pervasives.Native.option Armada.Base.pc_t Armada.State.Mkt Armada.State.__proj__Mkt__item__initial_tid Armada.State.__proj__Mkt__item__uniqs_used Armada.State.__proj__Mkt__item__mem Armada.State.__proj__Mkt__item__trace Armada.State.__proj__Mkt__item__stop_reason Spec.Map.t Armada.Thread.t Spec.Map.upd Armada.State.__proj__Mkt__item__threads Armada.Thread.Mkt Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__top Armada.Thread.__proj__Mkt__item__stack Armada.Thread.__proj__Mkt__item__write_buffer Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers
let update_thread_pc_in_state (s: Armada.State.t) (tid: tid_t) (opc: option pc_t) : Armada.State.t =
  
match opc with
| Some pc ->
  let thread = s.threads tid in
  let new_thread = { thread with pc = pc } in
  let new_threads = Spec.Map.upd s.threads tid new_thread in
  { s with threads = new_threads }
| None -> s