module TransitionSystemModule {
  var action: enum { A };
  var nondet_1: enum { A };
  var x: integer;

  init {
    x = 3;

  }
  next {
    havoc nondet_1;
    action' = nondet_1;
    if (action == A) {
      x' = (2 * x);
    } else {
      x' = (x + 1);
    }

  }
  invariant spec: (x >= 0);

}
