/* This file was generated by Contract AspectJ v0.1 on Sat Nov 06 14:08:33 EST 2004 */
 /** CONAJ: Original packages **/
package jsim.event;
 /** CONAJ: Imports needed by CONAJ  **/
 import org.aspectj.lang.*; 
 import java.util.*;
 /** CONAJ: Original imports **/



	 privileged aspect Event_Contract {
	 declare parents : Event implements Cloneable;
	public Object Event.clone(){
		 try { 
			return super.clone();
				 } catch (Exception e){
					 System.out.println(" Error in cloning method");
					 e.printStackTrace();
					 return new Object(); 
				}
			}
		
		Event old;
					 pointcut scope(): !within(Event_Contract) && !cflow(withincode(* Event_Contract.*(..)));
					 pointcut Event_occur1(Event trg_instance):call( public * Event.occur(..))
							 && !call(public * (Event+ && !Event).occur(..)) && target(trg_instance) && scope();

			 pointcut cast_Event_occur1(Event trg_instance):!(call( public * Event.occur(..)))
							 && execution(public * Event.occur(..)) && !execution( public * (Event+ && !Event).occur(..)) && target(trg_instance) && scope();

 // PCD for Invariant
			 pointcut Event_invariant(Event trg_instance):call(public * Event.*(..)) && !call(public * (Event+ && !Event).*(..)) && target(trg_instance) && scope();

		before(Event trg_instance):
			Event_invariant(trg_instance){
				if (!checkInvariant(trg_instance)){
					System.out.println("error in inv before a method call");
					System.exit(1);
				}
			}
		
		
		
		after(Event trg_instance):
			Event_invariant(trg_instance){
				if (!checkInvariant(trg_instance)){
					System.out.println("error in inv after a method call");
					System.exit(1);
				}
			}
		
 public boolean checkInvariant(Event trg_instance){
			if (trg_instance.counter>=0) {
			 return true;
			} else { 
			 return false;
			}

		}
	
	
	
	}