namespace cruise.umple.nusmv;

use NuSMVMetamodel.ump;

class NuSMVCoordinator
{
  depend cruise.umple.compiler.*;
  depend java.util.*;
  depend com.google.common.collect.ArrayListMultimap;
  depend com.google.common.collect.Multimap;
	space <<!

!>>
  output <<!-- This file is generated from <<=model.getUmpleFile().getFileName()>> --!>>
  emit commentModel(UmpleModel model)(output,space); 
  
  	/**
  * This changes the first caharacter of a given string.
  * @param str the given string.
  * @param index value 0 - Lowercase, 1 - Uppercase, Otherwise no change
  * @return the resulting string value.
  */
  public String changeNameCase(String str , int index) {
    	char[] stringArray = str.trim().toCharArray();
    	if(index == 1)
    		stringArray[0] = Character.toUpperCase(stringArray[0]);
    	if(index == 0)
    		stringArray[0] = Character.toLowerCase(stringArray[0]);
    	str = new String(stringArray);
    	return str;
  	}
  	
  	public boolean isNested(StateMachine sm) {
  		boolean yes = false;
  		for(State st : sm.getStates()) 
  			if(st.numberOfNestedStateMachines() > 0) {
  				yes = true;
  				break;
  			}
  		return yes;
  	}
  	
  	public StringBuilder generateSystem( List<NuSMVModule> modules ) {
  		StringBuilder temp = new StringBuilder();
  		for( NuSMVModule mod : modules )
  			temp.append(mod.toString()+"\n");
  		return temp;
  	}
  	  	
  	private NuSMVModule generateParentModule( StateMachine sm, UmpleClass uClass ) {
  		  		
		VarDeclaration vdec = new VarDeclaration( getStateList( sm ) );
		vdec.addVariableSpecifier( getEventList( sm ) );
		for( VariableSpecifier vs : generateSpecifiersForAttributesOf( uClass ) )
			vdec.addVariableSpecifier(vs);
		ModuleBody body = new ModuleBody( vdec );
  		body.addModuleElement( vdec );
		
  		//Adding define declaration to module body
  		body.addModuleElement( getDefineDeclaration(sm) );
  		body.addModuleElement( getAssignConstraint( sm, sm) );
		body.addModuleElement( getEventAssignConstraint(sm) );
		
		//Adding assign constraints for all the attributes
		for( AssignConstraint constraint : getAssignConstraint( uClass ))
			body.addModuleElement( constraint );
		
  		NuSMVModule module = new NuSMVModule( changeNameCase( sm.getFullName(), 1 ), body );
  		generateParameters( module, sm, sm ); 
  		return module;
  	}
  	
	private <E> boolean has( Collection<E> objectList, E whatToFind ) {
  		boolean yes = false;
  		for(E st : objectList) {
  			if( st.equals(whatToFind) ) {
  				yes = true;
  				break;
  			}
  		}
  		return yes;
	}
	
	//Building dependency set 
	private List<String> getDependencySet( StateMachine root, StateMachine sm) {
		List<StateMachine> smList = generateStateMachineList( root );
		List<String> temp = new ArrayList<String>();
		if( root.equals(sm) ) {
			for(StateMachine stm : smList) 
				if( !stm.getFullName().equals(sm.getFullName()) ) 
					temp.add( stm.getFullName() );
		}
		else {
			temp.add( changeNameCase(root.getFullName(), 0) );
			State parent = getParentState(sm); 
			if( !parent.getStateMachine().equals(root) )
					temp.add( parent.getStateMachine().getFullName() );
		}
		return temp;
	}
	
	private State getParentState(StateMachine sm) {
			State bioParent = sm.getParentState();
			State gParent = sm.getParentState().getStateMachine().getParentState();
			if( gParent != null && gParent.isIsConcurrent() )
				return gParent;
			return bioParent;	
	}
  	
  	private void generateParameters( NuSMVModule module, StateMachine parent, StateMachine sm ) {
		List<String> dependencySet = getDependencySet( parent, sm);
		for(String stm : dependencySet) 
			module.addParameter( "_"+changeNameCase(stm,0) );
  	}
  	
	private VariableSpecifier generateVariableSpecifierForMain( StateMachine sm, StateMachine root ) {
		String identifier = changeNameCase( sm.getFullName(), 0);
		VariableSpecifier vs = new VariableSpecifier(identifier);
		List<String> dependencySet = getDependencySet( root, sm);
		for( String stm : dependencySet ) 
			vs.addTypeSpecifier( changeNameCase(stm,0) );
		vs.setIsBracketed(true);
		vs.setTypeName( changeNameCase(sm.getFullName(), 1) );
		return vs;
	}
	
	//Created to generate the list of state machine
	private List<StateMachine> generateStateMachineList( StateMachine root ) {
		List<StateMachine> nestedMachines = new ArrayList<StateMachine>();
		if(root.getParentState() == null)
			nestedMachines.add(root);
  		for( State st :  getCompositeStates(root) )
			for( StateMachine stm : getEmbeddedStateMachines(st) )
					nestedMachines.add( stm );
		return nestedMachines;
	}
	
	//Computes the list of embeddedStateMachines of a composite state
	private List<StateMachine> getEmbeddedStateMachines( State state ) {
		List<StateMachine> nestedMachines = new ArrayList<StateMachine>();
 
		for( StateMachine stm : state.getNestedStateMachines() ) {
			if(!state.isIsConcurrent()){
				if(!has(nestedMachines, stm))
					nestedMachines.add( stm );
				if( isNested( stm ) )
					for( StateMachine innerMachine : generateStateMachineList( stm ) )
							nestedMachines.add( innerMachine );
			}
			else {
				//skips the wrapper of the region
				if( stm.getImmediateNestedStateMachines().size() == 0 )
					nestedMachines.add( stm );
				
				for( StateMachine region : stm.getImmediateNestedStateMachines() ){
					if(!has(nestedMachines, stm)){
						nestedMachines.add( region );
						if( isNested( region ) )
							for( StateMachine innerMachine : generateStateMachineList( region ) )
								nestedMachines.add( innerMachine );
					}
				}
				if( stm.getImmediateNestedStateMachines().size() > 1 )
					nestedMachines.add( stm );
			}
		}
		return nestedMachines;	
	}
	
	private boolean isHighLevelTransition( Transition transition ){
		State source = transition.getFromState();
		if( source != null && source.hasNestedStateMachines() )
			return true;
		return false;
	}
	
	private StateMachine getStateMachineOfHighLevelTransition( Transition transition ){
		if( !isHighLevelTransition(transition) )
			return null;
		StateMachine source = transition.getFromState().getStateMachine();
		if( !isConcurrent(transition.getFromState()) )
			return source;
		return source.getImmediateNestedStateMachines().get(0);
	}
	
	private List<State> getCompositeStates(StateMachine sm) {
		List<State> temp = new ArrayList<State>();
		for(State st : sm.getStates())
			if(st.hasNestedStateMachines())
				temp.add(st);
		return temp;				
	}
	
	private List<NuSMVModule> generateModuleForCompositeStatesOf( StateMachine root, StateMachine parent ) {
		List<NuSMVModule> nestedMachines = new ArrayList<NuSMVModule>();
  		for( StateMachine stm : generateStateMachineList(root) ) {
			if( !stm.equals( root ) ) {
				NuSMVModule module = generateModuleForSubstate(stm, root);
				generateParameters( module, root, stm ); 
				nestedMachines.add( module );
			}
		}
		return nestedMachines;
	}
  	
  	public List<NuSMVModule> generateModuleForNestedStateMachine( StateMachine sm, UmpleClass uClass ) {
  		List<NuSMVModule> temp = new ArrayList<NuSMVModule>();
  		//Generates the parent state machine  		
  		NuSMVModule module = generateParentModule( sm, uClass );
  		temp.add(module);
  		for( NuSMVModule mod : generateModuleForCompositeStatesOf( sm, sm ) )
  			temp.add( mod );
			
		//Generating the main module for the statemachine
  		ModuleBody body = new ModuleBody(genMainVariableFor( sm ));
		for( StateMachine smm : generateStateMachineList( sm ) )
			generateSpecForStateReachability( smm, body );
		generateSpecForTransitionDeterminism( sm, body);
		NuSMVModule mainmodule = new NuSMVModule("main", body);	
		temp.add(mainmodule);
  		return temp;
  	}
  	
  	//This generates modules generated from a simple state machine including its main
  	public List<NuSMVModule> generateModuleForSimpleStateMachine( StateMachine sm, UmpleClass uClass ) {
  
  		List<NuSMVModule> temp = new ArrayList<NuSMVModule>();
  		//Generating and setting the parent module
  		temp.add( generateParentModule(sm, uClass) );
  		
  		//Generating the main module for the statemachine
  		ModuleBody body = new ModuleBody(genMainVariableFor( sm ));
  		NuSMVModule module = new NuSMVModule("main", body);	
  		generateSpecForStateReachability( sm, body ); 
		generateSpecForTransitionDeterminism(sm, body);
  		temp.add( module );
  		return temp;
  	}
  	
  	//This generates a module for a substate given the state machine of the state and the root state machine
  	public NuSMVModule generateModuleForSubstate( StateMachine sm, StateMachine root ) {
  		ModuleBody body = new ModuleBody( new VarDeclaration(getStateList(sm)) );
  		//Adding define declaration to module body
  		body.addModuleElement( getAssignConstraint( sm, root) );
  		NuSMVModule module = new NuSMVModule( changeNameCase(sm.getFullName(),1), body );	
  		return module;
  	}
  	
  	private int getObjectIdentity( StateMachine sm, Object obj) {
  		int pos = 1;
		if( obj instanceof Transition ){
			for(Transition trans : sm.getAllTransitions() ) {
				//System.out.println( trans.getEvent().getName()+"["+trans.getFromState().getName() +" -- "+trans.getNextState().getName()+"]");
				if(trans.equals( (Transition) obj) )
					return pos;
				pos++;
			}
			//System.out.println( ((Transition)obj).getEvent().getName()+"["+((Transition)obj).getFromState().getName() +" -- "+((Transition)obj).getNextState().getName()+"]");
		}
		if( obj instanceof Guard ) {
			pos = 1;
			for(Guard guard : sm.getAllGuards() ) {
				if(guard.equals(( Guard ) obj ))
					return pos;
				pos++;
			}
		}
  		return -1;
  	}
  	
  	private void generateSpecForStateReachability( StateMachine sm, ModuleBody body ) {
  		
  		for( State st : sm.getStates() ) {
  			BasicExpression bexp1 = new BasicExpression(changeNameCase(sm.getFullName(), 0)+".state");
    		BasicExpression bexp2 = new BasicExpression(changeNameCase(st.getStateMachine().getFullName(),1)+"_"+st.getName());
    		CTLExpression cexp = new CTLExpression("ctl");
    		cexp.addChild(bexp1);
    		cexp.addChild(bexp2);
    		cexp.setOperator(BasicExpression.Operator.EQ);
    		cexp.setBracketed(true);
    		cexp.setQualified(true);
    		cexp.setCtlOperator(CTLExpression.CtlOperator.EF);
    		CTLSpecification cspec = new CTLSpecification(cexp);
    		body.addModuleElement(cspec);
    	}
  	}
	
	/*private void generateSpecForTransitionDeterminism( StateMachine sm, ModuleBody body ) {
  		int i = 1;
  		while( i <= sm.getAllTransitions().size() ) {
			int j = i + 1;
			while( j <= sm.getAllTransitions().size() ) {
				BasicExpression bexp1 = new BasicExpression(changeNameCase(sm.getFullName(), 0)+".t"+i);
				BasicExpression bexp2 = new BasicExpression(changeNameCase(sm.getFullName(), 0)+".t"+j);
				BasicExpression bexp3 = new BasicExpression("temp");
				bexp3.addChild(bexp1);
				bexp3.addChild(bexp2);				
				
				CTLExpression cexp = new CTLExpression("ctl");
				cexp.addChild(bexp3);
				cexp.addChild( generateDestinationStatesExpr( mapIdentity( sm, i), mapIdentity( sm, j) ));
				cexp.setOperator( BasicExpression.Operator.IMPLY );
				cexp.setBracketed(true);
				cexp.setQualified(true);
				cexp.setCtlOperator(CTLExpression.CtlOperator.AG);
				
				CTLSpecification cspec = new CTLSpecification(cexp);
				body.addModuleElement(cspec);
				j++;
			}
			i++;
    	}
  	}*/
	
	private void generateSpecForTransitionDeterminism( StateMachine sm, ModuleBody body ) {
  		
		for(State st : sm.getStates() ) {
			for( Map.Entry<Transition,Transition> map : matchMakeTransitions(st).entries() ){
				Transition key = map.getKey();
				int i = getObjectIdentity( sm, key );
				Transition value = map.getValue();
				int j = getObjectIdentity( sm, value );
				BasicExpression bexp1 = new BasicExpression(changeNameCase(sm.getFullName(), 0)+".t"+i);
				BasicExpression bexp2 = new BasicExpression(changeNameCase(sm.getFullName(), 0)+".t"+j);
				BasicExpression bexp3 = new BasicExpression("temp");
				bexp3.addChild(bexp1);
				bexp3.addChild(bexp2);				
				
				CTLExpression cexp = new CTLExpression("ctl");
				cexp.addChild(bexp3);
				cexp.addChild( generateDestinationStatesExpr( mapIdentity( sm, i), mapIdentity( sm, j) ));
				cexp.setOperator( BasicExpression.Operator.IMPLY );
				cexp.setBracketed(true);
				cexp.setQualified(true);
				cexp.setCtlOperator(CTLExpression.CtlOperator.AG);
				
				CTLSpecification cspec = new CTLSpecification(cexp);
				body.addModuleElement(cspec);
			}
		}
  	}
	//scans through the list and returns true whenever what to find is contained in the list
	private <Transition> boolean has( Multimap<Transition,Transition> objectList, Map.Entry<Transition,Transition> whatToFind ) {
  		boolean yes = false;
  		for(Map.Entry<Transition,Transition> map : objectList.entries()) {
  			if( (map.getKey().equals(whatToFind.getKey()) && map.getValue().equals(whatToFind.getValue()))
				|| (map.getValue().equals(whatToFind.getKey()) && map.getKey().equals(whatToFind.getValue())) ) {
  				yes = true;
  				break;
  			}
  		}
  		return yes;
	}
	
	//match making 
	private void match( List<Transition> first, List<Transition> second, Multimap< Transition,Transition > pairable, boolean defaulted ) {
		int i = 0;
		int x = first.size(), y = second.size(); 
		if( !defaulted ) 
			x = x - 1;
		while( i < x ) {
			int j = 0;
			if( !defaulted ) 
				j = i + 1;
			while( j < y ) {
				Map.Entry<Transition, Transition> entry = new AbstractMap.SimpleEntry<Transition, Transition>( first.get(i), second.get(j));
				if( !has( pairable, entry ) && !entry.getKey().equals(entry.getValue()) )
					pairable.put( entry.getKey(), entry.getValue() );
				j++;
			}
			i++;
		}
	}
	
	private Multimap< Transition,Transition > matchMakeTransitions( State state ) {

		Multimap< Transition,Transition > pairable = matchMaker( state );
		int i = 0;	
		while( i < getEmbeddedStates( state ).size() ) {
			for( Map.Entry<Transition,Transition> map : matchMaker( getEmbeddedStates( state ).get(i) ).entries() )
				if(! has( pairable, map ) && !map.getKey().equals(map.getValue()) )
					pairable.put( map.getKey(), map.getValue() );
			i++;
		}
		return pairable;
	}
	
	//Constructs a map of pairable transitions
	private Multimap< Transition,Transition > matchMaker( State state ) {
		Multimap< Transition,Transition > pairable = ArrayListMultimap.create();
		List<Transition> outgoingTransitions = new ArrayList<Transition>();
		
		if( state.getNestedStateMachines().size() == 0 ) {
			for( Transition transition : state.getStateMachine().getAllTransitions() )
				if( transition.getFromState().equals( state ) && !has( outgoingTransitions, transition ) )
					outgoingTransitions.add( transition );
			match( outgoingTransitions, outgoingTransitions, pairable, false );
		}
		else if( state.getNestedStateMachines().size() >= 1 ) {
			
			List<Transition> highLevelTransitions = new ArrayList<Transition>();
			List<Transition> embeddedTransitions = new ArrayList<Transition>();			
			
			//------------------------ extracting highlevel transitions of a composite state ------------------------- 
			for( Transition transition : state.getStateMachine().getAllTransitions() ) {
				if( transition.getFromState().equals( state ) && !has( highLevelTransitions, transition ))
					highLevelTransitions.add( transition );
				
				for( State embeddedState : getEmbeddedStates( state ) )  
					if( transition.getFromState().equals( embeddedState ) )
						embeddedTransitions.add( transition );				
			}
			match( highLevelTransitions, embeddedTransitions, pairable, true );
			
			//------------------------ ending extraction of highlevel transitions for composite state ------------------------- 
			
			if( state.getNestedStateMachines().size() > 1 ) {
				StateMachine parent = state.getStateMachine();
				List<Transition> allOutGoingTransitions = new ArrayList<Transition>();
				
				//------------------------ extracting pairable set of outgoing transitions for an orthogonal state ------------------------- 
				for( State embeddedState : getEmbeddedStates( state ) ) { 
					List<Transition> outgoing = isOutgoingOfOrthogonal( embeddedState, state );
					for( Transition trans : outgoing )
						if( !has( allOutGoingTransitions, trans ) )
							allOutGoingTransitions.add( trans );
					List<Transition> external = new ArrayList<Transition>();
					for( Transition trans : parent.getAllTransitions() )
						if( has( getExternalStateOf( embeddedState, state ), trans.getFromState() ) ) //&& !has( allOutGoingTransitions,trans )
							external.add( trans );
					match( outgoing, external, pairable, true );
				}
				//------------------------ ending extraction -------------------------
				
				//------------------------ managing and-cross transitions -------------------------
				List<Transition> andCross = getAndCross( state );
				for( Transition trans : andCross ) {
					State source = trans.getFromState();
					List<State> external = getExternalStateOf( source, state );
					for( Transition tr : state.getStateMachine().getAllTransitions() )
						if( has( external, tr.getFromState() ) ) {
							Map.Entry<Transition, Transition> entry = new AbstractMap.SimpleEntry<Transition, Transition>( trans, tr);
							if( !has( pairable, entry ) && !entry.getKey().equals( entry.getValue() ) )
								pairable.put( entry.getKey(), entry.getValue() );
						}
					for( Transition tr : highLevelTransitions ){
						Map.Entry<Transition, Transition> entry = new AbstractMap.SimpleEntry<Transition, Transition>( trans, tr);
							if( !has( pairable, entry ) && !entry.getKey().equals(entry.getValue()) )
								pairable.put( entry.getKey(), entry.getValue() );
					}
				}
				//------------------------ ending and-cross management -------------------------
			}
		}
		
		return pairable;
	}
	
	private List<State> getEmbeddedStates(State state ) {
		List<State> embeddedStates = new ArrayList<State>();
		for( StateMachine smm : state.getNestedStateMachines() ) {
			for( State innerState : smm.getStates() ) {
				embeddedStates.add( innerState );
				for( State st : getEmbeddedStates(innerState) )
					embeddedStates.add( st ); 
			}
		}
		return embeddedStates;
	} 
	
	/*private List<State> getEmbeddedStates(State state ) {
		List<State> embeddedStates = new ArrayList<State>();
		for( StateMachine smm : getEmbeddedStateMachines( state ) )
			for( State embeddedState : getEmbeddedStates( smm ) ) 
				embeddedStates.add( embeddedState );
		return embeddedStates;
	}*/ 
	
	//Determines if a transition is an out-going transition of a concurrent state
	private List<Transition> isOutgoingOfOrthogonal( State state, State parent ) {
		List<State> embeddedStates = getEmbeddedStates( parent );
		StateMachine sm = parent.getStateMachine();
		List<Transition> outGoingTransitions = new ArrayList<Transition>();
		for( Transition transition : sm.getAllTransitions() )
			if( transition.getFromState().equals( state ) && !has( embeddedStates, transition.getNextState()))
				outGoingTransitions.add( transition );
		return outGoingTransitions;
	}
	
	//composing the set u(z,s) of states 
	private List<State> getExternalStateOf(State child, State parent ) {
		StateMachine sm = child.getStateMachine();
		List<State> closRelations = getEmbeddedStates( sm );
		List<State> states = new ArrayList<State>();
		for( State state : getEmbeddedStates( parent ) )
			if(! has( closRelations, state ))
				states.add( state );
		return states;
	}
	
	private Transition mapIdentity( StateMachine root, int id ) {
		
		for( Transition tr : root.getAllTransitions() )
			if( getObjectIdentity( root, tr ) == id )
				return tr;
		return null;
	}
	
	private StateMachine skipWrapper( StateMachine sm ){
		if( sm.getImmediateNestedStateMachines().size() == 1 && sm.getStates().size() > 0 )
			return sm.getImmediateNestedStateMachines().get( 0 );
		return sm;
		
	}
	
	private CTLExpression generateDestinationStatesExpr( Transition first, Transition second ) {
				
		BasicExpression f1 = new BasicExpression( changeNameCase( first.getNextState().getStateMachine().getFullName(), 0)+".state" );
    	BasicExpression f2 = new BasicExpression( changeNameCase( first.getNextState().getStateMachine().getFullName(),1)+"_"+first.getNextState().getName());
		BasicExpression firstExpr = new BasicExpression("first");
		firstExpr.addChild(f1);
		firstExpr.addChild(f2);
		firstExpr.setOperator(BasicExpression.Operator.EQ);
		
		BasicExpression s1 = new BasicExpression( changeNameCase( second.getNextState().getStateMachine().getFullName(),0)+".state" );
    	BasicExpression s2 = new BasicExpression( changeNameCase( second.getNextState().getStateMachine().getFullName(),1)+"_"+second.getNextState().getName());
		BasicExpression secondExpr = new BasicExpression("second");
		secondExpr.addChild(s1);
		secondExpr.addChild(s2);
		secondExpr.setOperator(BasicExpression.Operator.EQ);
		
		CTLExpression cexp = new CTLExpression("ctl");
		cexp.addChild( firstExpr );
		cexp.addChild( secondExpr );
		cexp.setOperator(BasicExpression.Operator.AND);
		cexp.setBracketed(true);
		cexp.setCtlOperator( CTLExpression.CtlOperator.EX );
		cexp.setQualified(true);
		
		return cexp;
	}
  	
  	private AssignConstraint getAssignConstraint( StateMachine sm, StateMachine root) {
  		BasicExpression bexp;
  		if( sm.getParentState() == null )
  			bexp = new BasicExpression(changeNameCase(sm.getFullName(),1)+"_"+sm.getStartState().getName());
  		else 
  			bexp = new BasicExpression("null");
			
  		InitAssign ia = new InitAssign("state", bexp);
  		AssignConstraint ac = new AssignConstraint(ia);
  		ac.addAssign(getNextAssign( sm, root ));
  		return ac;
  	}
	
	private AssignConstraint getEventAssignConstraint( StateMachine sm) {

		VariableSpecifier eventset = new VariableSpecifier("events");
		for( Event event : sm.getAllEvents() )
			eventset.addTypeSpecifier( "ev_"+event.getName() );
			
		BasicExpression lhs = new BasicExpression( sm.getFullName()+"_stable" );
    	BasicExpression rhs = new BasicExpression( "{ "+eventset.print()+" }" );
		CaseStatement stable = new CaseStatement(lhs, rhs);
			
		//defining otherwise case
		BasicExpression bexp1 = new BasicExpression("ev_null");
    	BasicExpression bexp2 = new BasicExpression("TRUE");
		CaseStatement otherwise = new CaseStatement(bexp2, bexp1);
		
		CaseExpression expr = new CaseExpression("",stable);
    	expr.addCaseStatement( otherwise );	
		NextAssign na = new NextAssign("event", expr);
	
  		BasicExpression bexp = new BasicExpression("ev_null");
  		InitAssign ia = new InitAssign("event", bexp);
  		AssignConstraint ac = new AssignConstraint( ia );
  		ac.addAssign( na );
  		return ac;	
  	}
	
	private List<AssignConstraint> getAssignConstraint( UmpleClass uClass ) {
		List<AssignConstraint> constraints = new ArrayList<AssignConstraint>();
		
		for( Attribute attribute : uClass.getAllAttributes() ) {
			BasicExpression bexp = new BasicExpression("");
			
			if( attribute.getValue() != null ){
				String value = attribute.getValue();
				switch( value ){
					case "true" : bexp = new BasicExpression("TRUE"); break;
					case "false" : bexp = new BasicExpression("FALSE"); break;
					default : bexp = new BasicExpression(value);
				}
			}
			else if( attribute.getValue() == null && (attribute.getType().equals("Boolean") || attribute.getType().equals("boolean")))
				bexp = new BasicExpression("FALSE");
			else if( attribute.getValue() == null && (attribute.getType().equals("Integer") || attribute.getType().equals("int")
				|| attribute.getType().equals("long") || attribute.getType().equals("Long") 
				|| attribute.getType().equals("short") || attribute.getType().equals("Short")))
				bexp = new BasicExpression("0");
			else if( attribute.getValue() == null && (attribute.getType().equals("Float") || attribute.getType().equals("float") 
				|| attribute.getType().equals("double") || attribute.getType().equals("Double")))
				bexp = new BasicExpression("0.0");
			
			InitAssign initialVal = new InitAssign(attribute.getName(), bexp);
			AssignConstraint assignConstraint = new AssignConstraint( initialVal );
			constraints.add( assignConstraint );
		}
  		return constraints;
  	}
	
	private CaseStatement initializeCompositeStartState( State state ) {
		
		BasicExpression bexp3 = new BasicExpression( "expr" );
		
		if( state.isIsStartState() && state.getStateMachine().getParentState() != null ) {
			State bioparent = getParentState(state.getStateMachine());
  			BasicExpression bexp1 = new BasicExpression("_"+changeNameCase(bioparent.getStateMachine().getFullName(), 0)+".state");
  			BasicExpression bexp2 = new BasicExpression(changeNameCase(bioparent.getStateMachine().getFullName(),1)+"_"+bioparent.getName());
			BasicExpression bexp7 = new BasicExpression( "expr" );
			bexp7.addChild( bexp1 );
  			bexp7.addChild( bexp2 );
  			bexp7.setOperator( BasicExpression.Operator.EQ );
			
			BasicExpression bexp4 = new BasicExpression("state");
			BasicExpression bexp5 = new BasicExpression("null");
			BasicExpression bexp6 = new BasicExpression("temp");
			bexp6.setOperator( BasicExpression.Operator.EQ );
			bexp6.addChild( bexp4 );
  			bexp6.addChild( bexp5 );
			
			bexp3.addChild(bexp7);
			bexp3.addChild(bexp6);
			bexp3.setOperator( BasicExpression.Operator.AND );
			
			BasicExpression st = new BasicExpression( changeNameCase(state.getStateMachine().getFullName(),1)+"_"+state.getName() ); 
			return new CaseStatement( bexp3, st );
  		}
		return null;		
	}
	
	//Disabling a composite state alone without other concurrent states
	private CaseStatement diasableCompositeState( State state ) {
		
		BasicExpression bexp3 = new BasicExpression( "expr" );
		
		if( state.isIsStartState() && state.getStateMachine().getParentState() != null ) {
			State bioparent =  getParentState(state.getStateMachine());
  			BasicExpression bexp1 = new BasicExpression("_"+changeNameCase(bioparent.getStateMachine().getFullName(), 0)+".state");
  			BasicExpression bexp2 = new BasicExpression(changeNameCase(bioparent.getStateMachine().getFullName(),1)+"_"+bioparent.getName());
			bexp3.addChild( bexp1 );
  			bexp3.addChild( bexp2 );
  			bexp3.setOperator( BasicExpression.Operator.NE );
			
			BasicExpression st = new BasicExpression( "null" ); 
			return new CaseStatement( bexp3, st );
  		}
		return null;		
	}
  	
  	private NextAssign getNextAssign( StateMachine sm, StateMachine root ) {
  		BasicExpression bexp1 = new BasicExpression("state");
    	BasicExpression bexp2 = new BasicExpression("TRUE");
    	CaseStatement temp = new CaseStatement(bexp2, bexp1);
    	CaseExpression expr = new CaseExpression("",temp);
		
		//*****changes made here....
		if( sm.getParentState() != null && getCaseStatementForNullState(sm, root) != null )
			expr.addCaseStatement( getCaseStatementForNullState(sm, root) );
		
    	for(State st : sm.getStates() ) {
    		CaseStatement cstatement = getCaseStatement(sm, st, root);
    		if( cstatement != null)
    			expr.addCaseStatement(cstatement);
    	}
		
		//Initializing and disabling composite states
		for(State st : sm.getStates() )
			if( initializeCompositeStartState( st ) != null )
				expr.addCaseStatement( initializeCompositeStartState( st ) );
				
		CaseStatement otherwise = new CaseStatement(bexp2, bexp1);
    	expr.addCaseStatement( otherwise );
    	expr.removeCaseStatement(temp);
		
    	NextAssign na = new NextAssign("state", expr);
    	return na;
  	}
		
	//Harvesting transitions for any given orthogonal state or region
	public List<Transition> getAllTransitionsForOrthogonalState( State st ) {
		List<Transition> results = new ArrayList<Transition>();
		if( !st.isIsConcurrent() )
			for( StateMachine sm : st.getNestedStateMachines() ) 
				for( Transition trans : getAllEnablingTransitions( sm ) )
					results.add( trans );
		return results;
	}
	
	//Harvesting transitions for a state machine
	//Also generates a list of next transitions for a state and its substates (where possible).
  	//That is transition that enables or activates a state
	private List<Transition> getAllEnablingTransitions( Object obj ) {
		List<Transition> results = new ArrayList<Transition>();
		if( obj instanceof StateMachine ){
			
			for( State st : ( (StateMachine) obj).getStates() ) {
				for( Transition trans : st.getNextTransition() )
					results.add( trans );
				if( st.hasNestedStateMachines() )
					for( StateMachine smm : st.getNestedStateMachines() )
						for( Transition transition : getAllEnablingTransitions( smm ) )
							results.add( transition );
			}
		}
		else if( obj instanceof State ){
			if( !((State) obj).hasNestedStateMachines() ) {
				return ((State) obj).getNextTransition();
			}
			else {
				for( Transition tr : ((State) obj).getNextTransition() )
					results.add(tr);
				for( StateMachine smm : ((State) obj).getNestedStateMachines() )
					for( Transition transition : getAllEnablingTransitions( smm ) )
						results.add( transition );
			}
		}
		return results;
	}
	
	private List<StateMachine> getNestedStateMachines(State state){
		if(!state.hasNestedStateMachines())
			return null;
		List<StateMachine> stateMachines = new ArrayList<StateMachine>();
		if(!state.isIsConcurrent())
			for(StateMachine sm : state.getNestedStateMachines())
				stateMachines.add(sm);
		else {
			//skips the wrapper of the region
			for(StateMachine nsm : state.getNestedStateMachines()) {
				System.out.println( nsm.getFullName() );
				if( nsm.getImmediateNestedStateMachines().size() != 1 )
					stateMachines.add(nsm);
				for( StateMachine region : nsm.getImmediateNestedStateMachines() ){
					stateMachines.add(region);
				}
			}
		}
		return stateMachines;	
	}
	
	//This method the set of and-cross transitions for a state machine
	private List<Transition> andCross(StateMachine sm) {
		
		List<State> embeddedStates = getEmbeddedStates(sm);
		List<State> friendStates = new ArrayList<State>();
		State parent = getParentState(sm);
		for(StateMachine smm : parent.getNestedStateMachines()) {
		
			//skipping the wrapper of regions
			for(StateMachine region : smm.getImmediateNestedStateMachines())
				if( !region.equals(sm) )
					for(State st : getEmbeddedStates(smm))
						if( !has( friendStates, st))
							friendStates.add(st);
		}
		
		List<Transition> andCrossTransitions = new ArrayList<Transition>();
		for( Transition tr : sm.getAllTransitions() ) {
		
			//defines a constraint for and-cross transitions
			if(!has(embeddedStates, tr.getNextState()) && has(friendStates, tr.getNextState()))
				andCrossTransitions.add(tr);
		}
		return andCrossTransitions;
	}
	
	//This computes and-cross transitions of a given state.
	private List<Transition> getAndCross( State state ) {
		List<Transition> andCross = new ArrayList<Transition>();
		if( ! state.isIsConcurrent() )
			return andCross;
		
		for( StateMachine sm : state.getNestedStateMachines() )
			for( Transition transition : andCross( sm ) )
				andCross.add( transition );
		return andCross;
	}
	
	private List<Transition> getEnclosedTransitions( State state ) {
	
		List<Transition> enclosedTransitions = new ArrayList<Transition>();
		for( Transition tr : getAllEnablingTransitions( state ) )
			if( !tr.getNextState().equals( state ))
				enclosedTransitions.add( tr );
		return enclosedTransitions;
	}
	
	//Computes the exit transitions for a concurrent region
	private List<Transition> getExitTransitionsForConcurrentRegion(StateMachine region, StateMachine root){
		List<Transition> trans = getEnclosedTransitions( getParentState(region) );
		List<Transition> temp = new ArrayList<Transition>();
		
		for( Transition tr : root.getAllTransitions() )
			if( !has( trans, tr ) )
				temp.add( tr ); //adds to temp every other transitions not enclosed by the parent state 
	
		//adding and-cross transitions for a given region
		List<State> embeddedStates = getEmbeddedStates( region );
		for( Transition tr : getAndCross( getParentState( region ) ) )
			if( !has( embeddedStates, tr.getNextState() ) )
				temp.add(tr);
		return temp;
	}
	
	//Computes exit transitions for non-orthogonal composite state
	private List<Transition> getExitTransitions(State st, StateMachine root) {
		List<Transition> transitions = new ArrayList<Transition>();
		for( Transition transition : root.getAllTransitions() ){
			if(st.hasNestedStateMachines() && !st.isIsConcurrent() )				
				for( StateMachine sm : st.getNestedStateMachines() ){
					List<State> embeddedStates = getEmbeddedStates(sm);
					if(!has(embeddedStates, transition.getNextState()) && !has(transitions,transition))
						transitions.add(transition);
						
					//This section handles nested regions
					for( StateMachine region : sm.getImmediateNestedStateMachines() )
						if( region.getParentState() != null )
							for( Transition tr : getExitTransitions(region.getParentState(), root))
								if(!has(embeddedStates, transition.getNextState()) && !has(transitions,transition))
									transitions.add(transition);
				}
		}
		return transitions;
	}
	
	private List<State> getEmbeddedStates(StateMachine sm ) {
		List<State> embeddedStates = new ArrayList<State>();
		for(State state : sm.getStates() ) {
			if(!state.hasNestedStateMachines())
				embeddedStates.add(state);
			else
				for( StateMachine stm : generateStateMachineList(sm) )
					for(State st : getEmbeddedStates(stm))
						embeddedStates.add(st);						
		}
		return embeddedStates;
	}
	
	public void printList( List<Transition> input, StateMachine root ) {
		String results = "";
		for( Transition element : input )
			results += getObjectIdentity( root, element ) +" ";
		System.out.println( results );
	}
	
	//****on-going work here -- disables non-orthogonal region
	private CaseStatement getCaseStatementForNullState( StateMachine sm, StateMachine root ) {
			
		int counter = 0;
		BasicExpression rt = new BasicExpression("root");
		List<Transition> trans;
		if(!( getParentState( sm ).isIsConcurrent() )) {
			if( sm.equals(root) ) return null;
			trans = getExitTransitions( getParentState( sm ), root );
		}
		else
			trans = getExitTransitionsForConcurrentRegion(sm, root);

		for( Transition tr : trans ) {
			BasicExpression bexp;
			bexp = new BasicExpression("_"+changeNameCase(root.getFullName(),0)+".t"+getObjectIdentity( root, tr) );	
			rt = getExpressionTreeFor( rt, bexp );
			counter++;
		}
		if(counter > 0) {
  			BasicExpression state = new BasicExpression( "null" ); 
  			return new CaseStatement( rt, state );
  		}
  		return null;
	}
  	
  	private CaseStatement getCaseStatement( StateMachine sm, State st, StateMachine parent ) {
  		int counter = 0;
  		BasicExpression root = new BasicExpression("root");
  		for( Transition tr : getAllEnablingTransitions(st) ) {
			
			//System.out.println( tr.getEvent().getName()+"["+tr.getFromState().getName() +" -- "+tr.getNextState().getName()+"]");
			BasicExpression bexp;
			if(!parent.equals(sm))
				bexp = new BasicExpression("_"+changeNameCase(parent.getFullName(),0)+".t"+getObjectIdentity( parent, tr) );	
			else	
				bexp = new BasicExpression("t"+getObjectIdentity( parent, tr) );
  			root = getExpressionTreeFor( root, bexp );	
  			counter++;
  		} 			
  		if(counter > 0) {
  			BasicExpression state = new BasicExpression( changeNameCase(st.getStateMachine().getFullName(),1)+"_"+st.getName() ); 
  			return new CaseStatement( root, state );
  		}
  		return null;
  	}
  	
  	//This adds expression to activate a composite start state
  	public Stack<State> ancestorStack( State st ) {
		if(st.getStateMachine().getParentState() == null)
			return null;
		Stack<State> ancestors = new Stack<State>();
		ancestors.push(st);
		State parent = st.getStateMachine().getParentState();
		while( parent != null && parent.isIsStartState() ) {
			ancestors.push(parent);
			parent = parent.getStateMachine().getParentState();
		}
		return ancestors;		
	}
  	
  	private BasicExpression getExpressionTreeFor( BasicExpression root, BasicExpression bexp ) {
  		if( root.getChildren().size() < 2) {
  			root.addChild(bexp); 
  			root.setOperator(BasicExpression.Operator.OR);
  		}
  		else {
  			BasicExpression temp = new BasicExpression(root.getChildren().get(0).getIdentifier());
  			temp.addChild(root.getChildren().get(0));
  			temp.addChild(bexp);
  			temp.setOperator(BasicExpression.Operator.OR);
  			root.addChild(temp);
  		}
  		return root;
  	}
  	
  	private VarDeclaration genMainVariableFor( StateMachine sm ) {
  		VariableSpecifier vs = new VariableSpecifier(changeNameCase(sm.getFullName(), 0));	
  		vs.addTypeSpecifier( changeNameCase(sm.getFullName(), 1));
  		VarDeclaration vdec = new VarDeclaration(vs); 
  		if(!isNested(sm)) 
  			return vdec;
		List<StateMachine> smList = generateStateMachineList( sm );	
  		for( StateMachine smm : smList ) {
  			VariableSpecifier vss = generateVariableSpecifierForMain( smm, sm );
  			vdec.addVariableSpecifier(vss);
  		}
		vdec.removeVariableSpecifier( vs );
  		return vdec;
  	}
  	
  	//Generates event enumeration for a given state machine
  	private  VariableSpecifier getEventList( StateMachine sm ) {
		
  		VariableSpecifier vs = new VariableSpecifier("event");
  		for( Event event : sm.getAllEvents() ) 
  			vs.addTypeSpecifier("ev_"+event.getName());
  		vs.addTypeSpecifier("ev_null");
  		return vs;
  	}
  	
  	//Generates state enumeration for a given state machine
  	private VariableSpecifier getStateList(StateMachine sm) {
  		VariableSpecifier vs = new VariableSpecifier("state");
  		for(State st : sm.getStates())
  			vs.addTypeSpecifier(changeNameCase(st.getStateMachine().getFullName(),1)+"_"+st.getName());
  		if(sm.getParentState() != null || sm.getStates().size() == 1)
  			vs.addTypeSpecifier("null");
  		return vs;
  	}
	
	private List<VariableSpecifier> generateSpecifiersForAttributesOf( UmpleClass uClass ){
		List<VariableSpecifier> attributes = new ArrayList<VariableSpecifier>();
		
		for( Attribute attribute : uClass.getAllAttributes() ){
			VariableSpecifier vs = new VariableSpecifier( attribute.getName() );
			String type = attribute.getFullType();
			//System.out.println( attribute.getValue() );
			switch( type ){
				case "Float" : vs.addTypeSpecifier("real"); attributes.add( vs ); break; 
				case "Boolean" : vs.addTypeSpecifier("boolean"); attributes.add( vs ); break;
				case "Integer" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				case "Long" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				case "long" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				case "Short" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				case "short" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				case "Double" : vs.addTypeSpecifier("real"); attributes.add( vs ); break;
				case "double" : vs.addTypeSpecifier("real"); attributes.add( vs ); break;
				case "float" : vs.addTypeSpecifier("real"); attributes.add( vs ); break; 
				case "boolean" : vs.addTypeSpecifier("boolean"); attributes.add( vs ); break;
				case "int" : vs.addTypeSpecifier("integer"); attributes.add( vs ); break;
				default : ;
			}
		}
		return attributes;
	}
  		
  	//Generates the define part for all the transitions of the system
  	private DefineDeclaration getDefineDeclaration( StateMachine sm ) {
  		BasicExpression temp = composeExpressionForStability(sm);
  		DefineBody stable = new DefineBody(sm.getFullName()+"_stable", temp);
  		DefineDeclaration ddec = new DefineDeclaration(stable);
  		for( Transition tr : sm.getAllTransitions() ) {
  			BasicExpression bexp = composeExpressionFor( tr, sm );
  			DefineBody dBody = new DefineBody("t"+getObjectIdentity( sm, tr) , bexp);
  			ddec.addDefineBody(dBody);
  		}
		for( Guard gr : sm.getAllGuards() ) {
  			DefineBody dBody = new DefineBody("g"+getObjectIdentity( sm, gr) , generateRHS( gr ));
  			ddec.addDefineBody(dBody);
  		}
  		//ddec.removeDefineBody(dnull);
  		return ddec;
  	}
	
	private boolean isConcurrent(State state){
		State parent = state.getStateMachine().getParentState();
		if( parent != null)
			if(parent.isIsConcurrent())
				return true;
		return false;
	}
  	
  	private BasicExpression composeExpressionFor( Transition tr, StateMachine sm ) {
  		BasicExpression bexp1 = new BasicExpression("event");
  		BasicExpression bexp2 = new BasicExpression("ev_"+tr.getEvent().getName());
  		BasicExpression bexp3 = new BasicExpression("eventExpr"); 
  		bexp3.addChild(bexp1);
  		bexp3.addChild(bexp2);
  		bexp3.setOperator(BasicExpression.Operator.EQ);
  		
  		BasicExpression bexp4 = generateRHS(tr.getFromState(), tr);
		BasicExpression bexp5;
		BasicExpression bexp6 = new BasicExpression("stateExpr");
		if( isHighLevelTransition(tr) && isConcurrent(tr.getFromState())) {
			bexp5 = new BasicExpression("null");
			bexp6.setOperator(BasicExpression.Operator.NE); 
		}
		else {	
			bexp5 = new BasicExpression(changeNameCase(tr.getFromState().getStateMachine().getFullName(),1)+"_"+tr.getFromState().getName());
			bexp6.setOperator(BasicExpression.Operator.EQ); 
		}
  		bexp6.addChild(bexp4);
  		bexp6.addChild(bexp5); 
  			
  		BasicExpression bexp = new BasicExpression("state");
  		bexp.addChild(bexp3);
  		bexp.addChild(bexp6);
		
		BasicExpression fBexp = new BasicExpression("fExp");
		fBexp.setOperator( BasicExpression.Operator.AND );
		if( tr.getGuard() != null ) {
			BasicExpression guard = new BasicExpression("g"+getObjectIdentity( sm, tr.getGuard()));
			fBexp.addChild(bexp);
			fBexp.addChild(guard);
			return fBexp;
		}
  		  		
  		return bexp;
  	}
	
	private BasicExpression composeExpressionForStability( StateMachine sm ) {
		BasicExpression root = new BasicExpression("root");
		for(Event event : sm.getAllEvents() ){
			BasicExpression bexp1 = new BasicExpression("event");
			BasicExpression bexp2 = new BasicExpression("ev_"+event.getName());
			BasicExpression bexp3 = new BasicExpression("eventExpr"); 
			bexp3.addChild(bexp1);
			bexp3.addChild(bexp2);
			bexp3.setOperator(BasicExpression.Operator.EQ);
			root = getExpressionTreeFor( root, bexp3 );
		}
		root.setDisplayNegation(true);
		root.setBracketed(true);
  		return root;
  	}
	
  	
  	private BasicExpression generateRHS( Object obj, Transition tr ) {
  		BasicExpression bexp4 = null;
		if( obj instanceof State ) {
			State st = ( State ) obj;
			State state = st.getStateMachine().getParentState(); 
			if( state != null ) {
				StateMachine sm;
				if( !isHighLevelTransition(tr) )
					sm = st.getStateMachine();
				else
					sm = getStateMachineOfHighLevelTransition(tr);
				String name = changeNameCase(sm.getFullName(), 0);
				bexp4 = new BasicExpression("_" +name + ".state"); 
			}
			else 
				bexp4 = new BasicExpression("state");
		}
  		return bexp4;
  	}
	
	private BasicExpression generateRHS( Guard guard) {
		return new BasicExpression( getExpression( guard.getQueuedExpression() ) );
  	}
	
	//checks the input string and reports if it is an operator or not
	private boolean isOperator(String variable){
		switch( variable ){
			case "+" : return true;
			case "-" : return true;
			case "*" : return true;
			case "/" : return true;
			case "%" : return true;
			case "&&" : return true;
			case "||" : return true;
			case "==" : return true;
			case "!=" : return true;
			case ">=" : return true;
			case "<=" : return true;
			case "<" : return true;
			case ">" : return true;
			case ">>" : return true;
			case "<<" : return true;
			case "+=" : return true;
			case "-=" : return true;
			case "*=" : return true;
			case "%=" : return true;
			case "/=" : return true;
			case ">>=" : return true;
			case "<<=" : return true;
			//case "^" : return true;
			default : return false;
		}		
	}
	
	public String getExpression( ArrayDeque<String> nodes ) {
		String temp = "", lastVariable = "";
		while( nodes.size() > 1) {
			String variable = nodes.poll();
			if( isOperator(variable) )
				temp += " "+ mapOperator( variable ) +" ";
			else	
				temp += variable;
			lastVariable = variable;
		}
		temp += mapOperator( nodes.poll() );
		return temp;	
	}
	
	private String mapOperator( String value ) {
		switch( value ) {
			case "&&" : return "&";
			case "||" : return "|";
			case "%" : return "mod";
			case "==" : return "=";
			//case "object==" : return "=";
			case "true" : return "TRUE";
			case "false" : return "FALSE";
			default : return value;
		}
	}
  }