spec module Ensemble {
    default I = Init;
    default padRead(f, p1, p2) = f & 
               card(p1)=1 & (p1 in Skratch_pad.Init) & (p1 in Skratch_pad.Read) & 
               card(p2)=1 & (p2 in Skratch_pad.Init) & (p2 in Skratch_pad.Read);

    specvar Init : bool;
    specvar INITIA : bool;
    specvar PREDIC : bool;
    specvar INTRAF : bool;
    specvar CORREC : bool;
    specvar BNDRY : bool;
    specvar VIR : bool;
    specvar INTERF : bool;
    specvar SCALEFORCES : bool;
    specvar KINETI : bool;

    format INITIAH_temp;

    // We're going to use scopes as follows.
    // The current spec should be the spec as seen from Main.
    // However, the state as seen from inside the Computations
    // scope will have Molecule objects (which belong to arrays)
    // transitioning between the different typestates.
    proc init(input_name:string) suspends I
      requires not Init
      modifies Init, H2O.Init, Skratch_pad.Init, Simparm.Init, Simparm.ParmsLoaded, Atom.Init
      calls Vec, Acc_double, Skratch_pad, Simparm, H2O 
      ensures Init';
    proc getMolecule(idx:int) returns rv:Molecule ensures (rv' in H2O.Init) & card(rv')=1;

    proc getKinetiMolecule(idx:int) returns rv:Molecule 
      requires KINETI 
      ensures (rv' in H2O.Init) & (rv' in H2O.Kineti) & card(rv') = 1;
    proc getBndryMolecule(idx:int) returns rv:Molecule
      requires BNDRY
      ensures (rv' in H2O.Init) & (rv' in H2O.Bndry) & card(rv') = 1;
    proc getPredicScaledMolecule(idx:int) returns rv:Molecule
      requires PREDIC
      ensures (rv' in H2O.Init) & (rv' in H2O.Predic) & 
              (rv' in H2O.Scaled) & card(rv') = 1;
    proc getPredicMolecule(idx:int) returns rv:Molecule 
      requires PREDIC 
      ensures (rv' in H2O.Init) & (rv' in H2O.Predic') & card(rv') = 1;
    proc getCorrecMolecule(idx:int) returns rv:Molecule 
      requires CORREC 
      ensures (rv' in H2O.Init) & (rv' in H2O.Correc') & card(rv') = 1;

    proc getPad(idx:int) returns rv:Pad ensures (rv' in Skratch_pad.Init) & card(rv')=1;

    proc INITIA()
      modifies INITIA,H2O.Vel,H2O.Pos calls Vec, Simparm, C, H2O ensures INITIA';
    private proc INITIAH(t:INITIAH_temp;
                 XS:float; NS:float; ZERO:float; WSIN:float; WCOS:float) 
      calls H2O, C
      ensures true;
    private proc INITIAM(random_numbers:in_channel; t:P; SUM:P) 
      requires (card(t) = 1) & (t in H2O.Vel)
      calls Vec, H2O ensures true;
    private proc INITIAEND(SUM:P; SU:P; XMAS:float[]; t1:P; t:P) 
      requires card(t1)=1
      modifies H2O.Vel, H2O.Pos
      calls C, Vec, H2O, Simparm ensures true;

    private proc loadData()
      modifies Skratch_pad.Read, Skratch_pad.Updated, H2O.Pos, H2O.Vel
      calls Skratch_pad ensures true;
    private proc interfOuterDispatch()
      modifies Skratch_pad.Updated ensures true;
    private proc interfOuterLoop()
      modifies Skratch_pad.Updated ensures true;
    private proc interfInnerLoop(idx:int)
      modifies Skratch_pad.Updated ensures true;
    private proc storeData(dest:int) calls H2O ensures true;
    private proc interf2(p1:Pad; p2:Pad) 
      modifies Skratch_pad.Updated
      calls Skratch_pad, Acc_double 
      ensures true;
    private proc interf2_aux(p1:Pad; p2:Pad; t:interf2_temp) returns rv:float
      calls Vec, C, Simparm 
      ensures true;

    proc CSHIFT2(p1:Pad; p2:Pad; t:CS2_L;S:float[]) 
      calls Skratch_pad, Vec
      ensures true;
    private proc clearTVIR() ensures true;
    private proc updateTVIR() ensures true;
    private proc clearTKIN() ensures true;
    private proc updateTKIN() ensures true;

    proc SCALEFORCES(Dest:int) requires INTERF & PREDIC
      modifies H2O.Scaled, H2O.Predic, SCALEFORCES
      calls Simparm, H2O 
      ensures SCALEFORCES';
      // MDMAIN calls stepsystem...
    proc MDMAIN() requires INITIA
      modifies Atom.Correc, Atom.Predic, H2O.Correc, H2O.Predic,
               INTRAF, H2O.Intraf, Skratch_pad.Read, 
               Skratch_pad.Updated, H2O.Pos, H2O.Vel,
               H2O.Bndry, H2O.Kineti, H2O.Scaled, SCALEFORCES,
               VIR, INTERF, CORREC, BNDRY, KINETI, PREDIC
      calls Simparm ensures true;

    // --- MAIN LOOP -------------------------------------------------------
    proc stepsystem() requires INITIA 
      modifies Atom.Correc, Atom.Predic, H2O.Correc, H2O.Predic,
               INTRAF, H2O.Intraf, Skratch_pad.Read, 
               Skratch_pad.Updated, H2O.Pos, H2O.Vel,
               H2O.Bndry, H2O.Kineti, H2O.Scaled, SCALEFORCES,
               VIR, INTERF, CORREC, BNDRY, KINETI, PREDIC
      calls Acc_double, Simparm, C ensures true;

    proc dummy_PREDIC() modifies PREDIC ensures PREDIC';

    proc PREDIC()
      modifies Atom.Correc, Atom.Predic, H2O.Correc, H2O.Predic, PREDIC
      calls Simparm, H2O ensures PREDIC';
    proc INTRAF() 
      requires INITIA & PREDIC
      modifies INTRAF, H2O.Intraf, H2O.Predic
      calls H2O ensures INTRAF';
    proc computeVIR() requires INTRAF modifies VIR calls H2O ensures VIR';
    proc INTERF(DEST:int) requires VIR
      modifies INTERF, Skratch_pad.Read, Skratch_pad.Updated, H2O.Pos, H2O.Vel
      ensures INTERF';
    proc CORREC() requires INTERF & PREDIC
      modifies Atom.Correc, Atom.Predic, H2O.Correc, 
               H2O.Predic, H2O.Scaled, CORREC
      calls Simparm, H2O ensures CORREC';
    proc BNDRY(size:float) requires CORREC
      modifies H2O.Correc, H2O.Bndry, BNDRY
      calls H2O ensures BNDRY';
    proc KINETI() requires BNDRY
      modifies H2O.Bndry, H2O.Kineti, KINETI calls H2O, Vec ensures KINETI';

    proc POTENG() 
      modifies Skratch_pad.Read, Skratch_pad.Updated, H2O.Pos, H2O.Vel
      calls Vec, Simparm 
      ensures true;
    proc INTRA_POTENG() calls H2O ensures true;
    proc INTER_POTENG() 
      modifies Skratch_pad.Read, Skratch_pad.Updated, H2O.Pos, H2O.Vel 
      ensures true;
    proc potengOuterDispatch() ensures true;
    proc potengOuterLoop() ensures true;
    proc potengInnerLoop(idx:int) calls Vec ensures true;
    proc interPoteng2Aux(p1:Pad; p2:Pad; res:P) 
      calls Vec, Simparm ensures true;

    proc printENERGY(iter:int) calls Vec ensures true;
}