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

     (*
        Variable step_parameter' contains a record with field 'bindSet', which
        contains a set with input for the process. If 'bindSet' is 'Nil' return
        whole 'inputSet'
     *)
     ProcessParameterInput( inputSet ) == IF (CHOOSE s \in step_parameter': TRUE).bindSet = Nil
                                            THEN inputSet
					    ELSE (CHOOSE s \in step_parameter': TRUE).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 each record in the set in field '_rows' validates at least one row in 'inputParam'
          -- cardinality of inputParam[key] = cardinality _row.set

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

       Should be implemented using recursion, but at the time of writing this comment could not make it work.

     *)
     RECURSIVE ProcessParameterEnables( _, _ )
     ProcessParameterEnables( inputParam, bindDefs ) == ( \A key \in  { k \in DOMAIN bindDefs : k # "_key" /\ k # "_rows" }:  bindDefs[key] = inputParam[key]  )
                   /\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_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] : 
                      Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\  \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef ) 
	           )


    (* ProcessParameterBind operator
       
       Bind 'inputParam' for the process currently being executed with values in 'step_parameter'.

       Bind to inputParameter allowed if one the following matches
           - step parameter WildCard
           - process parameter = WildCard
           - predicate 'ProcessParameterEnables' resolves TRUE for some paramter set in 'step_parameter'
	   
       *)
     ProcessParameterBind( inputParam ) == step_parameter' = WildCard 
                       \/ { processEnabledInStep \in step_parameter' : 
                              processEnabledInStep.process = step' 
                              /\ ( processEnabledInStep.bindRule = WildCard 
                                   \/ ProcessParameterEnables( inputParam, processEnabledInStep.bindRule ) )   } # {}