val make_successor_info (action_index path_index: nat) : armada_successor_info_t
val make_successor_info (action_index path_index: nat) : armada_successor_info_t
let make_successor_info (action_index: nat) (path_index: nat) : armada_successor_info_t =
  {
    action_index = action_index;
    path_index = path_index;
  }
module MyRegularToAtomicRefinement

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.Tactics.V2
open MyAtomicLProg
open MyLProg
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.RegularToAtomic.Armada
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.Nth
open Util.Range

// This is all the PCs in the program.

let my_lpcs: array_t pc_t = list_to_array [ "main.0"; "main.1"; "main.2"; "main.3"; "main.4"; "main.5" ]

// The start PC is "main.0", which is the 0th element of the my_lpcs array.

let my_lprog_main_start_pc_index = 0

// Every PC is breaking except "main.2" and "main.3":

let my_pc_index_breaking : array_t bool = list_to_array [ true; true; false; false; true; true ]

// The ten actions are:
// 0 - ok = true, start_pc = "main.0", end_pc = "main.1"
// 1 - ok = false, start_pc = "main.0", end_pc = "main.1"
// 2 - ok = true, start_pc = "main.1", end_pc = "main.2"
// 3 - ok = false, start_pc = "main.1", end_pc = "main.2"
// 4 - ok = true, start_pc = "main.2", end_pc = "main.3"
// 5 - ok = false, start_pc = "main.2", end_pc = "main.3"
// 6 - ok = true, start_pc = "main.3", end_pc = "main.4"
// 7 - ok = false, start_pc = "main.3", end_pc = "main.4"
// 8 - ok = true, start_pc = "main.4", end_pc = "main.5"
// 9 - ok = false, start_pc = "main.4", end_pc = "main.5"

let make_pc_indices (start_pc_index: nat) (end_pc_index: nat) : statement_pc_indices_t =
  {
    start_pc_index = Some start_pc_index;
    end_pc_index = Some end_pc_index;
    create_thread_initial_pc_index = None;
    method_call_return_pc_index = None;
  }

// This array gives the indices of the PCs mentioned in the ten actions.
// None of them are create-thread or method-call instructions, so they
// always use None for the last two fields of each statement_pc_indices_t.

let my_pc_indices_array: array_t statement_pc_indices_t = list_to_array
  [
    make_pc_indices 0 1; // Action 0 goes from "main.0" to "main.1"
    make_pc_indices 0 1; // Action 1 goes from "main.0" to "main.1"
    make_pc_indices 1 2; // Action 2 goes from "main.1" to "main.2"
    make_pc_indices 1 2; // Action 3 goes from "main.1" to "main.2"
    make_pc_indices 2 3; // Action 4 goes from "main.2" to "main.3"
    make_pc_indices 2 3; // Action 5 goes from "main.2" to "main.3"
    make_pc_indices 3 4; // Action 6 goes from "main.3" to "main.4"
    make_pc_indices 3 4; // Action 7 goes from "main.3" to "main.4"
    make_pc_indices 4 5; // Action 8 goes from "main.4" to "main.5"
    make_pc_indices 4 5  // Action 9 goes from "main.4" to "main.5"
  ]

// This is the list of action indices with a start_pc of None.  We don't have
// any in this program because we don't include tau.

let my_action_indices_starting_at_no_pc: list nat = []

// This is a list of, for each PC, the list of actions that start at that PC.

let my_action_indices_starting_at_pc_index: array_t (list nat) = list_to_array
  [
    [0; 1]; // The actions starting at "main.0" are actions 0 and 1
    [2; 3]; // The actions starting at "main.1" are actions 2 and 3
    [4; 5]; // The actions starting at "main.2" are actions 4 and 5
    [6; 7]; // The actions starting at "main.3" are actions 6 and 7
    [8; 9]; // The actions starting at "main.4" are actions 8 and 9
    []      // The actions starting at "main.5" are <empty set>
  ]
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.Armada.fsti.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyLProg.fst.checked MyAtomicLProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyRegularToAtomicRefinement.fst
action_index: Prims.nat -> path_index: Prims.nat
  -> Strategies.RegularToAtomic.Armada.armada_successor_info_t
Prims.nat Strategies.RegularToAtomic.Armada.Mkarmada_successor_info_t Strategies.RegularToAtomic.Armada.armada_successor_info_t
let make_successor_info (action_index path_index: nat) : armada_successor_info_t =
  
{ action_index = action_index; path_index = path_index }