spec module Main
{
  // the main procedure runs iteration #0 of the simulation
  // and passes control to MDMAIN to run the other iterations.
  proc main (args:string[]) 
    requires not Ensemble.Init
    modifies Ensemble.SCALEFORCES, Ensemble.INTERF, Ensemble.VIR,
             Ensemble.INTRAF, Ensemble.INITIA, Ensemble.Init,
             Ensemble.CORREC, Ensemble.BNDRY, Ensemble.KINETI,
             Ensemble.PREDIC
    calls Simparm, Ensemble, C
    ensures true;
}