Die Hard Jug example

[MikaelMayer]

Once we get proper model checking in Strata Core, I think we ought to be able to return a counter-example to the following program. Taken from a movie.

var bigJug := 0
var smallJug := 0
loop {
  if * {
    bigJug := 5
  } else if * {
    smallJug := 5
  } else if * {
    bigJug := smallJug
    smallJug := 0
  } else if * {
    if bigJug + smallJug <= 5 {
      bigJug := bigJug + smallJug
      smallJug := 0
    } else {
      var delta := bigJug + smallJug - 5
      bigJug := 5
      smallJug := delta
    }
  }
  assert bigJug != 4  // Find counter example and trace.
}

That could be part of our benchmarks for model checking. @tautschnig Thoughts?

[tautschnig]

Can we write this in a syntax that we support right now, like Laurel? The following should be close, but still doesn't pass laurel exe strata laurelParse:

procedure Jug() returns ()
{
  var bigJug: int := 0;
  var smallJug: int := 0;
  loop {
    if * {
      bigJug := 5;
    } else {
      if * {
        smallJug := 5;
      } else {
        if * {
          bigJug := smallJug;
          smallJug := 0;
        } else {
          if * {
            if bigJug + smallJug <= 5 {
              bigJug := bigJug + smallJug;
              smallJug := 0;
            } else {
              var delta: int := bigJug + smallJug - 5;
              bigJug := 5;
              smallJug := delta;
            }
          }
        }
      }
    }
    assert bigJug != 4  // Find counter example and trace.
  }
}