(* 
	 Current time in state variable now gets ticked
	 when process starts.
     *)
     currentTime == now

     (*
	 Return set of possible bindings to an enabled process

	 @param [Set] inputSet set of all possible inputs to a process
	 @return first that matches
	   - inputSet                if step_parameter.bindSet  == Nil
	   - step_parameter.bindSet  if step_parameter.bindSet  != Nil
     *)
     ProcessParameterInput( inputSet ) ==
	 IF step_parameter'.bindSet = Nil
	      THEN inputSet
	      ELSE step_parameter'.bindSet
		    
     (* All record fields in 'bindDef' must bind with corresponding fields in 'inputParam' *)
     \* ProcessParameterEnablesTst( inputParam, bindDefs ) == \A key \in  { k \in DOMAIN bindDefs : k # "_key" }:  bindDefs[key] = inputParam[key] 

     (*
       ProcessParameterEnables: 'inputParam' satisfies 'bindDefs'

       - all 'normal' field in 'bindDefs' are found in 'inputParam'
       - and all subrecords  can be validated recursively using 'ProcessParameterEnables' using a the set in field '_key'
       - and for each record in the set in field '_rows'
             -- validates at least one row in 'inputParam'
                --- cardinality of inputParam[key] = cardinality _row.set
	     -- OR  equals 'values' set

       Recurse one level down  in 'inputParam' using keys 'bindDefs._key.key'.
       Recursion is done only if 'bindDefs' defines field '_key'.


     *)
     RECURSIVE ProcessParameterEnables( _, _ )
     ProcessParameterEnables( inputParam, bindDefs ) ==
                      ( \A key \in  { k \in DOMAIN bindDefs : Len(k)<4 \/ (SubSeq(k,1,4) # "_key" /\ k # "_rows" )}:  bindDefs[key] = inputParam[key]  )
                   /\ ( \A reckey \in { k \in DOMAIN bindDefs : Len(k)>3 /\SubSeq(k,1,4)  = "_key"  }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
                   /\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
                              (r.row_types = "singletons" /\ r.set = inputParam[r.key]  )
                           \/ (r.row_types = "hashes" /\ Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\  \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef ) )
	              )


    (*
    
     Predicate to filter elements in ProcessParameterInput set to pass
     to +steps+ element in +step_parameter' variable.
     
     Pass +inputParameter+ to a process if one the following matches
	 - resume_contex # Nil (i.e. process execution is resuming)
	 - step_parameter = WildCard  (i.e. Head elemend of +steps+ sequence is WildCard, allow everything )
	 - step_parameter.bindSet = WildCard (i.e. Head element defines bindSet element)
	 - predicate 'ProcessParameterEnables' resolves TRUE for  step_parameter'.bindRule
     *)

     ProcessParameterBind( inputParam ) ==
		       \/  resume_context' # Nil
		       \/  step_parameter' = WildCard  
		       \/  step_parameter'.bindRule = WildCard
		       \/  ProcessParameterEnables( inputParam, step_parameter'.bindRule )