class Petition {
  
  string description;
  string title;
  string date;
  int signatures;
  boolean submitted;
  
  //@ invariant signatures >= 0;
  //@ initial signatures == 0 && !submitted;
  void Petition() {
	  title = "";
	  submitted = false;
  }
  
  //@ requires !submitted;
  //@ ensures !submitted;
  void setDescription (string d) {
    description = d;
  }
  
  //@ requires !submitted;
  //@ ensures !submitted;
  void setTitle (string t) {
    title = t;
  }
  
  //@ requires !submitted;
  //@ ensures !submitted;
  void setDueDate (string d) {
    date = d;
  }

  //@ requires !submitted;
  //@ ensures |result| -> submitted; 
  boolean submit () {
    submitted = true;
	
	submitted;
  }
  
  //@ requires submitted;
  //@ ensures submitted; 
  void sign (string name) {
    signatures = signatures + 1;
  }
  
  //@ requires submitted;
  //@ ensures submitted;     
  int howMany () {
    signatures;
  }   
  
  //@ requires true;
  //@ ensures |result| -> submitted;
  boolean isSubmitted() {
	  submitted;
  }
}

class Signatory {
  
  string name;
  Petition petition;
  boolean canSign;
  
  //@ invariant true;
  //@ initial !canSign;
  void Signatory (string n) {
    name = n;
	canSign = false;
  }
 
  //@ requires !canSign && p.isSubmitted();
  //@ ensures canSign;
  void setPetition (Petition p) {
    petition = p;
  }
  
  //@ requires true;
  //@ ensures true; 
  boolean canSignPetition() {
	canSign;
  }
  
  //@ requires canSign;
  //@ ensures canSign;
  void signPlease () {
    petition.sign(name);
	printStr(name);
	printStr(" signed and found");
	printStr(petition.howMany());
	printStr(" signatures\n");
  }
}

unrestricted class PetitionServer {
  
  int petitionsSoFar;
  
  //@ invariant true;
  //@ initial true;
  void petitionsSoFar () {
    petitionsSoFar = 0;
  }
 
  //@ requires true;
  //@ ensures true;
  Petition create () {
    petitionsSoFar = petitionsSoFar + 1;
	new Petition();
  }
}

class SaveTheWolf {
  
  Petition petition;
  Signatory signatory1;
  Signatory signatory2;
  boolean done;
  
  //@ invariant true;
  //@ requires !s1.canSignPetition() && !s2.canSignPetition();
  //@ initial !done;
  void SaveTheWolf (PetitionServer s, Signatory s1, Signatory s2) {
    petition = s.create();
	signatory1 = s1;
	signatory2 = s2;
	done = false;
  }
 
  //@ requires !done;
  //@ ensures done;
  void run () {
    petition.setDescription("Save the Iberian wolf");
    petition.setDueDate("11 October 2011");
    petition.setTitle("Save the Wolves");
    petition.setDueDate("11 November 2011");
	
	if (petition.submit()) {
	  signatory1.setPetition(petition);
	  spawn { signatory1.signPlease(); }
	  signatory2.setPetition(petition);
	  spawn { signatory2.signPlease(); }
	  petition.sign("Vasco");
	  printStr ("Vasco signed and found ");
	  printInt (petition.howMany());
	  printStr (" signatures\n");
	}
  }
}