spec module H2O {
    format Molecule;
    format P;
    format Pad;
    format A;

    specvar Init, Predic, Intraf, Scaled:Molecule set;
    specvar Correc, Bndry, Kineti, tvir:Molecule set;
    // note that adding the set 'tvir' causes crashage!

    default mInit(f, m) = f & (card(m)=1) & (m in Init);

    specvar Pos, Vel:P set;

    // m in H2O.Init implies m.h1, h.o, m.h2 in Atom.Init
    proc init(m:Molecule) 
      suspends mInit
      requires card(m)=1 & (not (m in Init)) 
      modifies Init, Atom.Init calls Atom ensures m in Init';

    private proc getH1(m:Molecule) returns rv:A
      ensures card(rv')=1 & (rv' in Atom.Init) &
              ((m in Predic) => (rv' in Atom.Predic)) & 
              ((m in Correc) => (rv' in Atom.Correc));

    private proc getO(m:Molecule) returns rv:A
      ensures card(rv')=1 & (rv' in Atom.Init) &
              ((m in Predic) => (rv' in Atom.Predic)) & 
              ((m in Correc) => (rv' in Atom.Correc));

    private proc getH2(m:Molecule) returns rv:A
      ensures card(rv')=1 & (rv' in Atom.Init) &
              ((m in Predic) => (rv' in Atom.Predic)) & 
              ((m in Correc) => (rv' in Atom.Correc));

    proc storeH1Pos(m:Molecule;v:P) 
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Pos';
    proc storeOPos(m:Molecule;v:P)
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Pos';
    proc storeH2Pos(m:Molecule;v:P)
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Pos';
    
    proc loadH1Vel(m:Molecule;v:P)
      requires card(v)=1 & (v in Vel) 
      calls Vec, C, Atom
      ensures true;
    proc loadOVel(m:Molecule;v:P)
      requires card(v)=1 & (v in Vel) 
      calls Vec, C, Atom
      ensures true;
    proc loadH2Vel(m:Molecule;v:P)
      requires card(v)=1 & (v in Vel) 
      calls Vec, C, Atom
      ensures true;
    
    proc storeH1Vel(m:Molecule;v:P) 
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Vel';
    proc storeOVel(m:Molecule;v:P)
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Vel';
    proc storeH2Vel(m:Molecule;v:P)
      requires card(v)=1 modifies Pos, Vel
      calls Vec, C, Atom ensures v in Vel';
    
    proc loadV(m:Molecule;v:P) 
      calls Vec ensures true;
    proc storeV(m:Molecule;v:P) 
      calls Vec ensures true;
    
    proc clear(m:Molecule) 
      calls Atom ensures true;

    /* predic -> intraf -> vir -> scale -> correc ->
     *   bndry -> kineti -> updateTVIR -> predic */
    proc predic(m:Molecule; n:int; c:float[]) 
      modifies Predic, Correc, Atom.Predic, Atom.Correc
      calls Atom
      ensures m in Predic';
  
    proc scaleMomenta(m:Molecule; dest:int; HM:float; OM:float)
      requires (m in Predic) 
      modifies Scaled, Predic calls Vec, Atom
      ensures (m in Scaled') & not (m in Predic');
  
    proc correc(m:Molecule; n:int; c:float[]) 
      requires (m in Scaled) & (m in Predic)
      modifies Predic, Correc, Atom.Predic, Atom.Correc, Scaled
      calls Atom
      ensures (m in Correc') & not (m in Scaled') & not (m in Predic');
  
    proc loadDirPos(m:Molecule; dir:int; v:float[])
      calls Vec, Atom, C
      ensures true;
  
    proc storeDirVel(m:Molecule; dir:int; v:P) 
      calls Vec, Atom, C
      ensures true;

    proc shiftAxis(m:Molecule; dir:int; v:float) 
      calls Vec, Atom, C
      ensures true;

    proc bndry(m:Molecule;b:float) 
      requires (m in Correc)
      modifies Correc, Bndry
      calls Vec, Atom, C
      ensures (m in Bndry') & not (m in Correc');
  
    proc kineti(m:Molecule;s:P)
      requires (m in Bndry)
      modifies Bndry, Kineti
      calls Vec, Atom, C
      ensures (m in Kineti') & not (m in Bndry');
  
    proc intra_poteng(m:Molecule;v:P) 
      calls Vec, Atom, C
      ensures true;

    proc vir(m:Molecule)
      calls Vec, Atom, C, Acc_double
      ensures true;
    
    proc intraf(m:Molecule)
      requires m in Predic
      modifies Intraf, Predic
      calls Vec, Atom, C
      ensures (m in Intraf');
  
    proc updateFields(m:Molecule;d:int; p:Pad)
      requires card(p) = 1 & (p in Skratch_pad.Init)
      calls Vec, Atom, Skratch_pad
      ensures true;

    proc dump(m:Molecule)
      calls Vec, Atom ensures true;

    proc makePos(v:P) requires card(v)=1
      modifies Pos,Vel ensures (Pos' = Pos + v) & (Vel' = Vel - v);
    proc makeVel(v:P) requires card(v)=1
      modifies Pos,Vel ensures (Vel' = Vel + v) & (Pos' = Pos - v);
}