
// Define the module
module main {
  // Shared variable
  var x : int;

  // Initialize the shared variable
  init {
    x = 3;
  }

  // Action A: x := 2 * x
  procedure actionA()
    modifies x;
  {
    x = 2 * x;
  }

  // Action B: x := x + 1
  procedure actionB()
    modifies x;
  {
    x = x + 1;
  }

  // Example interleavings
  // Interleaving 1: A followed by B
  procedure interleavingAB()
    modifies x;
  {
    call actionA();
    call actionB();
  }

  // Interleaving 2: B followed by A
  procedure interleavingBA()
    modifies x;
  {
    call actionB();
    call actionA();
  }

  // Main control block to invoke interleavings and check outcomes
  control {
    // Execute interleaving AB
    call interleavingAB();
    print x; // Print the outcome of x after interleaving AB
    reset;   // Reset the state of x to its initial value

    // Execute interleaving BA
    call interleavingBA();
    print x; // Print the outcome of x after interleaving BA
  }
}
