-- -- Copyright 2014 Alessandro Gerlinger Romero -- -- This file is part of Hybrid fUML. -- -- Hybrid fUML is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 3 of the License, or -- (at your option) any later version. -- -- Hybrid fUML is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with Hybrid fUML. If not, see . -- ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- Module: semanticMapping_main -- Import: syntax_abstractSyntax_embedded -- Import: syntax_abstractSyntax_profile -- Import: syntax_abstractSyntax_derivedFunctions -- Import: syntax_library_embedded -- Import: syntax_userModel_embedded -- Import: semanticDomain_embedded -- Import: semanticDomain_defined -- Import: semanticMapping ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- MAIN RULE rule_fUML_mainSyn :: Rule() rule_fUML_mainSyn = if not (emptyDom function_fUML_Agents) then -- (R) REACTION -- (RA) prepare reaction rule_fUML_prepareReaction `seq` -- (D) DISCRETE -- (DA) prepare a discrete step rule_fUML_prepareDiscreteStep `seq` ( -- (DB) it tests: discrete behavior evaluation should be done if function_fUML_executeDiscreteSteps l then -- (DC) evaluate discrete behavior until fix point iterate (multiDeterm function_fUML_Agents) else skip ) `seq` -- (DD) synchronize time bases rule_fUML_checkDiscreteStepsSync `seq` -- garbage collector rule_fUML_garbageCollector else skip where -- locus l = function_fUML_locus ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- INIT RULE -- create an agent for the activity main (must exist) -- receives -- reaction time -- discretizationstep -- evolveAutomatically rule_fUML_init :: Int -> Float -> Bool -> Rule() rule_fUML_init rt ds ea = if emptyDom function_fUML_Agents then let res = function_fUML_getResolutionPhysicalClk in do create l do create f do create ex do create mtb do -- creating an identifier for current evaluation function_fUML_evaluationId := primAsmRandom 999999999 -- locus's setup function_Locus_executor(l):= ex function_Locus_factory(l):= f -- setup executor function_Executor_locus(ex):= l -- setup factory function_ExecutionFactory_locus(f):= l -- VERY IMPORTANT -- IT MUST USE EVALUATION OF RULES IN SEQUENCE due to the fact of concurrent change in a function with domain object -- setuping types foldl1 (seq) $ (map (\pt -> do operatio_ExecutionFactory_addBuiltInType f pt ) [integer, boolean, string, unlimitedNatural, real]) -- setuping primitive behaviors foldl1 (seq) $ (map (\(cl, vt) -> do nv <- (rule_FUML_Semantics_Classes_Kernel_Value_create vt) function_Value_Object_types(nv) := {cl} operatio_ExecutionFactory_addPrimitiveBehaviorPrototype f nv ) [(primitiveBehaviorsminus_RealFunctionsminus_Neg, FUML_Implementation_Reals_RealNegExecution), (primitiveBehaviorsminus_RealFunctionsminus_minus, FUML_Implementation_Reals_RealMinusExecution), (primitiveBehaviorsminus_RealFunctionsminus_times, FUML_Implementation_Reals_RealMultExecution), (primitiveBehaviorsminus_RealFunctionsminus_plus, FUML_Implementation_Reals_RealAddExecution), (primitiveBehaviorsminus_RealFunctionsminus_le, FUML_Implementation_Reals_RealLessThanOrEqualExecution), (primitiveBehaviorsminus_BooleanFunctionsminus_And,FUML_Implementation_Booleans_BooleanAndExecution), (primitiveBehaviorsminus_BooleanFunctionsminus_Not,FUML_Implementation_Booleans_BooleanNotExecution) ]) -- setup default configuration function_Locus_evolvePhysicalClkAutomatically(l):= ea -- setup initial value for the edge function_Locus_physicalClkIsOnEdge(l):= False -- setup time reaction clock reactionClk <- (rule_FUML_Semantics_Extensions_Clock_Clock_create FUML_Semantics_Extensions_Clock_LogicalClock) reactionTimeBase <- (rule_FUML_Semantics_Extensions_Clock_TimeBase_create FUML_Semantics_Extensions_Clock_DiscreteTimeBase) ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Locus_reactionClock(l):= reactionClk function_Clock_timeBase(reactionClk):= reactionTimeBase function_Clock_resolution(reactionClk):= 1.0 function_Clock_LogicalClock_locus(reactionClk) := l function_Clock_LogicalClock_definingEvent(reactionClk) := function_Instance_Event_semanticEventForReactionClk function_TimeBase_owningMTB(reactionTimeBase):= mtb function_TimeBase_currentInstant(reactionTimeBase) := ri function_Instant_date(ri):=0.0 function_Instant_tb(ri):=reactionTimeBase -- setup time logical clock logicalClk <- (rule_FUML_Semantics_Extensions_Clock_Clock_create FUML_Semantics_Extensions_Clock_LogicalClock) logicalTimeBase <- (rule_FUML_Semantics_Extensions_Clock_TimeBase_create FUML_Semantics_Extensions_Clock_DiscreteTimeBase) li <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Locus_logicalClock(l):= logicalClk function_Clock_timeBase(logicalClk):= logicalTimeBase function_Clock_resolution(logicalClk):= 1.0 function_Clock_LogicalClock_locus(logicalClk) := l function_Clock_LogicalClock_definingEvent(logicalClk) := function_Instance_Event_semanticEventForLogicalClk function_TimeBase_owningMTB(logicalTimeBase):= mtb function_TimeBase_currentInstant(logicalTimeBase) := li function_Instant_date(li):=0.0 function_Instant_tb(li):=logicalTimeBase -- setup time physical clock physicalClk <- (rule_FUML_Semantics_Extensions_Clock_Clock_create FUML_Semantics_Extensions_Clock_PhysicalClock) physicalTimeBase <- (rule_FUML_Semantics_Extensions_Clock_TimeBase_create FUML_Semantics_Extensions_Clock_DiscreteTimeBase) pi <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Locus_physicalClock(l):= physicalClk function_Clock_timeBase(physicalClk):= physicalTimeBase -- setting the resolution for the physical clock -- if it is not defined by CCSL use the parameter if res == 0.0 then function_Clock_resolution(physicalClk):= ds else function_Clock_resolution(physicalClk):= res function_TimeBase_owningMTB(physicalTimeBase):= mtb function_TimeBase_currentInstant(physicalTimeBase) := pi function_Instant_date(pi):=0.0 function_Instant_tb(pi):=physicalTimeBase -- default multiple time base function_Locus_mainTimeBase(l):= mtb `seq` let l = function_fUML_locus in let f = function_Locus_factory l in let reactionClk = function_Locus_reactionClock l in let reactionPeriod = function_fUML_Clock_getPeriod reactionClk in do -- create an execution for the main (MANDATORY NAME) ex <- (operatio_ExecutionFactory_createExecution f main FUML_Semantics_Classes_Kernel_ValueEmpty) -- create agent function_fUML_Agents(ex):= operatio_Value_Execution_execute -- setting mode function_fUML_Agents_mode(ex) := FUML_Status_NotInitialized -- checking period for reaction clock if reactionPeriod == 0 then -- if it is not defined by CCSL function_Locus_defaultPeriod2ReactionClk(l):= rt else skip else skip -- used to pure discrete behavior rule_fUML_initSyn :: Rule() rule_fUML_initSyn = rule_fUML_init 0 0.0 False ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- PREPARE NEW REACTION rule_fUML_prepareReaction :: Rule() rule_fUML_prepareReaction = do -- remove old signals forall (v1,v2,cl,i) <- (expr2list $ dom function_fUML_signals) do if i < truncate rt then do -- removing signal function_fUML_signals(v1,v2,cl,i) := FUML_Semantics_Classes_Kernel_ValueEmpty rule_fUML_Value_CompoundValue_destroy (function_fUML_signals (v1,v2,cl,i)) else skip -- remove old instants forall tb <- expr2list owtbs do forall i <- (init (function_TimeBase_instants tb)) do function_Instant_date(i) := 0.0 function_Instant_tb(i):= FUML_Semantics_Extensions_Clock_TimeBaseEmpty -- indicating that edge should not be verified function_Locus_physicalClkIsOnEdge(l) := True -- checking agents forall a <- (expr2list $ dom function_fUML_Agents_mode) do -- allowing paused to continue (running) if (function_fUML_Agents_mode(a) == FUML_Status_Paused) then rule_fUML_activityExecution_resume a else skip -- allowing waiting blocked activities to continue monitoring the signal (not running) -- during the reaction, it shall be evaluated looking for their presence (HERE) if (function_fUML_Agents_mode(a) == FUML_Status_WaitingSignalBlocked) then function_fUML_Agents_mode(a) := FUML_Status_WaitingSignalTempBlocked else skip -- -- READING INPUT -- it shall be made available through external change of ASM's state -- `seq` do -- incrementing reaction clock ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_TimeBase_currentInstant(tb) := ri function_Instant_date(ri) := rt + 1.0 function_Instant_tb(ri):=tb -- if time should evolve alone (without signal) -- timed initialization if function_Locus_evolvePhysicalClkAutomatically l then -- note that, in this special case, two instants for the same clock are defined with the same value (just to mark that the time should evolve) -- it does not offer risk for the evolution of reactions -- call rule that increments clock rule_fUML_incrementEventClock l (function_Clock_LogicalClock_definingEvent rc) else skip `seq` -- showing current reaction -- stdout rule_fUML_out $ "rule_fUML_prepareReaction - reaction time: " ++ show (function_fUML_Clock_currentTimeInt rc) ++ " logical time: " ++ show (function_fUML_Clock_currentTimeInt lc) where -- locus l = function_fUML_locus -- rc = function_Locus_reactionClock l rt = function_Clock_currentTime rc tb = function_Clock_timeBase rc lc = function_Locus_logicalClock l -- range multipletimebase mtb = function_Locus_mainTimeBase l owtbs = function_MultipleTimeBase_ownedTBs mtb ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- PREPARE NEW DISCRETE STEP rule_fUML_prepareDiscreteStep :: Rule() rule_fUML_prepareDiscreteStep = if function_fUML_executeDiscreteSteps l then do -- checking agents forall a <- (expr2list $ dom function_fUML_Agents_mode) do -- allowing waiting blocked activities to continue monitoring the signal (not running) -- rationale: if a transfer function triggered by a discrete domain send a signal -- weakness: difficulty for causality check -- during the iteration for one reaction these signals can be generated (HERE) if (function_fUML_Agents_mode(a) == FUML_Status_WaitingSignalTempBlocked) then function_fUML_Agents_mode(a) := FUML_Status_WaitingSignal else skip -- verifying edge and allowing waiting edge agents to run only when the edge is reached (running) if (function_fUML_Agents_mode(a) == FUML_Status_WaitingEdgeValue && (function_Locus_physicalClkIsOnEdge l)) then rule_fUML_activityExecution_resume a else skip -- advance logical time ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_TimeBase_currentInstant(tb) := ri function_Instant_date(ri) := lt + 1.0 function_Instant_tb(ri):=tb else skip where -- locus l = function_fUML_locus -- lc = function_Locus_logicalClock l lt = function_Clock_currentTime lc tb = function_Clock_timeBase lc rc = function_Locus_reactionClock l rt = function_Clock_currentTime rc ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- CHECK -- just synchronize the time bases -- rule_fUML_checkDiscreteStepsSync :: Rule() rule_fUML_checkDiscreteStepsSync = -- synchronize all timebases forall c <- tbdsl do function_TimeBase_currentInstant(function_Clock_timeBase c) := last (function_TimeBase_instants (function_Clock_timeBase c)) where -- locus l = function_fUML_locus -- -- all logical clocks clocks = function_Locus_logicalClocks l -- -- defining if it has logical clock not pointing to the current instant tbdsl = filter (\cl -> function_fUML_Clock_isDesynchronized cl) $ expr2list clocks ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- GARBAGE COLLECTOR -- It removes unused objects rule_fUML_garbageCollector :: Rule() rule_fUML_garbageCollector = -- removing unused offers (forall o <- expr2list((dom function_Offer_offeredTokens) `difference` (bigUnion (ran function_ActivityEdgeInstance_offers))) do function_Offer_offeredTokens(o):= {}) `seq` -- removing unused objecttokens (forall t <- expr2list(((dom function_Token_ObjectToken_value) `difference` (bigUnion (ran function_ActivityNodeActivation_heldTokens))) `difference` (bigUnion $ ran function_Offer_offeredTokens)) do function_Token_ObjectToken_value(t):= FUML_Semantics_Classes_Kernel_ValueEmpty) `seq` let usedvalues = (ran function_fUML_signals) in -- removing unused signals (forall sv <- expr2list((dom function_Value_SignalInstance_type) `difference` usedvalues) do rule_fUML_Value_CompoundValue_destroy sv) `seq` -- removing unused datavalues (forall dv <- expr2list((dom function_Value_DataValue_type) `difference` usedvalues) do rule_fUML_Value_CompoundValue_destroy dv) `seq` rule_fUML_garbageCollectorPrimitiveTypes rule_fUML_garbageCollectorPrimitiveTypes :: Rule() rule_fUML_garbageCollectorPrimitiveTypes = let usedvalues = (ran function_Token_ObjectToken_value `union` (mkSet $ concat $ expr2list $ ran function_FeatureValue_values) `union` (bigUnion $ ran function_ParameterValue_values)) in -- removing unused realvalues (forall rv <- expr2list((dom function_Value_RealValue_value) `difference` usedvalues) do function_Value_RealValue_value(rv):= 0.0 function_Value_PrimitiveValue_type(rv):= FUML_Syntax_Classes_Kernel_ClassifierEmpty) `seq` -- removing unused booleanvalues (forall bv <- expr2list((dom function_Value_BooleanValue_value) `difference` usedvalues) do function_Value_BooleanValue_value(bv):= False function_Value_PrimitiveValue_type(bv):= FUML_Syntax_Classes_Kernel_ClassifierEmpty) `seq` -- removing unused integervalues (forall iv <- expr2list((dom function_Value_IntegerValue_value) `difference` usedvalues) do function_Value_IntegerValue_value(iv):= 0 function_Value_PrimitiveValue_type(iv):= FUML_Syntax_Classes_Kernel_ClassifierEmpty) `seq` -- removing unused primitivevalues (default value but not used) (forall ptv <- expr2list((dom function_Value_PrimitiveValue_type) `difference` usedvalues) do function_Value_PrimitiveValue_type(ptv):= FUML_Syntax_Classes_Kernel_ClassifierEmpty) `seq` -- removing unused referencevalues (forall refv <- expr2list((dom function_Value_Reference_referent) `difference` usedvalues) do function_Value_Reference_referent(refv):=FUML_Semantics_Classes_Kernel_ValueEmpty) ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- SUPPORT RULE -- redefinition of multi rule from AsmGofer, to enable all agents in parallel and get the effects of inconsistent updates (if they exist) multiDeterm :: AsmVar (a -> (a -> Rule ())) -> Rule () multiDeterm = multi' . assocs where multi' [] = skip multi' as = do let ((a,r):rs) = as secureCall (r a) multi' (rs) ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- SUPPORT FUNCTIONS -- -- used to check if it should execute discrete steps function_fUML_executeDiscreteSteps :: FUML_Semantics_Loci_LociL1_Locus -> Bool function_fUML_executeDiscreteSteps l = (card function_fUML_Agents_runnableInThisDiscreteEvaluation) > 0 || ( (function_Locus_physicalClkIsOnEdge l) && (function_fUML_Agents_hasRunnableWaitingEdge || function_fUML_Agents_hasRunnableWaitingSignalTempBlocked)) -- -- used to unique define an evaluation -- important for trace file generation function_fUML_evaluationId :: Dynamic Int function_fUML_evaluationId = initVal "function_fUML_evaluationId" 0