val atomic_actions:list (list Armada.Action.t)
val atomic_actions:list (list Armada.Action.t)
let atomic_actions: list (list Armada.Action.t) =
  [
    // Statement at PC 0 succeeds
    [
      {
        ok = true;
        program_statement = { start_pc = Some "main.0";
                              end_pc = Some "main.1";
                              starts_atomic_block = true;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "g"); }
      }
    ];

    // Statement at PC 0 exhibits undefined behavior
    [
      {
        ok = false;
        program_statement = { start_pc = Some "main.0";
                              end_pc = Some "main.1";
                              starts_atomic_block = true;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "g"); }
      }
    ];

    // Statements at PCs 1-3 run successfully
    [
      {
        ok = true;
        program_statement = { start_pc = Some "main.1";
                              end_pc = Some "main.2";
                              starts_atomic_block = true;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "c"); };
      };
      {
        ok = true;
        program_statement = { start_pc = Some "main.2";
                              end_pc = Some "main.3";
                              starts_atomic_block = false;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "b"); }
      };
      {
        ok = true;
        program_statement = { start_pc = Some "main.3";
                              end_pc = Some "main.4";
                              starts_atomic_block = false;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e"); }
      }
    ];

    // Statement at PC 1 exhibits undefined behavior
    [
      {
        ok = false;
        program_statement = { start_pc = Some "main.1";
                              end_pc = Some "main.2";
                              starts_atomic_block = true;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "c"); }
      }
    ];

    // Statement at PC 1 runs normally then statement at PC 2 exhibits undefined behavior
    [
      {
        ok = true;
        program_statement = { start_pc = Some "main.1";
                              end_pc = Some "main.2";
                              starts_atomic_block = true;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "c"); }
      };
      {
        ok = false;
        program_statement = { start_pc = Some "main.2";
                              end_pc = Some "main.3";
                              starts_atomic_block = false;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "b"); }
      }
    ];

    // Statements at PCs 1-2 run successfully then statement at PC 3 exhibits undefined behavior
    [
      {
        ok = true;
        program_statement = { start_pc = Some "main.1";
                              end_pc = Some "main.2";
                              starts_atomic_block = true;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "c"); }
      };
      {
        ok = true;
        program_statement = { start_pc = Some "main.2";
                              end_pc = Some "main.3";
                              starts_atomic_block = false;
                              ends_atomic_block = false;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "b"); }
      };
      {
        ok = false;
        program_statement = { start_pc = Some "main.3";
                              end_pc = Some "main.4";
                              starts_atomic_block = false;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "e"); }
      }
    ];

    // Statement at PC 4 runs normally
    [
      {
        ok = true;
        program_statement = { start_pc = Some "main.4";
                              end_pc = Some "main.5";
                              starts_atomic_block = true;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
                                (ExpressionBinaryOperator (ObjectTDAbstract int) (ObjectTDAbstract int) (ObjectTDAbstract int)
                                  BinaryOpDivInt
                                  (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
                                  (ExpressionGlobalVariable (ObjectTDAbstract int) "f")); }
      }
    ];

    // Statement at PC 4 exhibits undefined behavior
    [
      {
        ok = false;
        program_statement = { start_pc = Some "main.4";
                              end_pc = Some "main.5";
                              starts_atomic_block = true;
                              ends_atomic_block = true;
                              statement = UpdateStatement false
                                (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
                                (ExpressionBinaryOperator (ObjectTDAbstract int) (ObjectTDAbstract int) (ObjectTDAbstract int)
                                  BinaryOpDivInt
                                  (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
                                  (ExpressionGlobalVariable (ObjectTDAbstract int) "f")); }
      }
    ]
  ]
module MyAtomicHProg

open Armada.Action
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
/
Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyHProg.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Action.fst.checked
MyAtomicHProg.fst
Prims.list (Prims.list Armada.Action.t)
Prims.Cons Prims.list Armada.Action.t Armada.Action.Mkt Armada.Action.Mkprogram_statement_t FStar.Pervasives.Native.Some Armada.Base.pc_t Armada.Statement.UpdateStatement Armada.Expression.ExpressionGlobalVariable Armada.Type.ObjectTDAbstract Prims.int Prims.Nil Armada.Expression.ExpressionBinaryOperator Armada.BinaryOp.BinaryOpDivInt
let atomic_actions:list (list Armada.Action.t) =
  
[
  [
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.0";
        end_pc = Some "main.1";
        starts_atomic_block = true;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "g")
      }
    }
  ];
  [
    {
      ok = false;
      program_statement
      =
      {
        start_pc = Some "main.0";
        end_pc = Some "main.1";
        starts_atomic_block = true;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "g")
      }
    }
  ];
  [
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.1";
        end_pc = Some "main.2";
        starts_atomic_block = true;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "c")
      }
    };
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.2";
        end_pc = Some "main.3";
        starts_atomic_block = false;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "b")
      }
    };
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.3";
        end_pc = Some "main.4";
        starts_atomic_block = false;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
      }
    }
  ];
  [
    {
      ok = false;
      program_statement
      =
      {
        start_pc = Some "main.1";
        end_pc = Some "main.2";
        starts_atomic_block = true;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "c")
      }
    }
  ];
  [
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.1";
        end_pc = Some "main.2";
        starts_atomic_block = true;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "c")
      }
    };
    {
      ok = false;
      program_statement
      =
      {
        start_pc = Some "main.2";
        end_pc = Some "main.3";
        starts_atomic_block = false;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "b")
      }
    }
  ];
  [
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.1";
        end_pc = Some "main.2";
        starts_atomic_block = true;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "a")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "c")
      }
    };
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.2";
        end_pc = Some "main.3";
        starts_atomic_block = false;
        ends_atomic_block = false;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "d")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "b")
      }
    };
    {
      ok = false;
      program_statement
      =
      {
        start_pc = Some "main.3";
        end_pc = Some "main.4";
        starts_atomic_block = false;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
          (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
      }
    }
  ];
  [
    {
      ok = true;
      program_statement
      =
      {
        start_pc = Some "main.4";
        end_pc = Some "main.5";
        starts_atomic_block = true;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
          (ExpressionBinaryOperator (ObjectTDAbstract int)
              (ObjectTDAbstract int)
              (ObjectTDAbstract int)
              BinaryOpDivInt
              (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
              (ExpressionGlobalVariable (ObjectTDAbstract int) "f"))
      }
    }
  ];
  [
    {
      ok = false;
      program_statement
      =
      {
        start_pc = Some "main.4";
        end_pc = Some "main.5";
        starts_atomic_block = true;
        ends_atomic_block = true;
        statement
        =
        UpdateStatement false
          (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
          (ExpressionBinaryOperator (ObjectTDAbstract int)
              (ObjectTDAbstract int)
              (ObjectTDAbstract int)
              BinaryOpDivInt
              (ExpressionGlobalVariable (ObjectTDAbstract int) "f")
              (ExpressionGlobalVariable (ObjectTDAbstract int) "f"))
      }
    }
  ]
]