model GoPFMetaModel

-- classes

class PF
attributes
  name : String
operations
  patternCollection(): Set (Pattern) = self.pattern
  isEqualTo(g:PF):Boolean = 
	((self.name = g.name) and 
	(self.pattern->forAll(p1|g.pattern->exists(p2|p2.isEqualTo(p1)))) and 
	(g.pattern->forAll(p1|self.pattern->exists(p2|p2.isEqualTo(p1)))))
end

class Pattern
attributes
  name : String
operations
  replaceGMBB(g:GoalModelBB):Boolean
  addBizS(b:BusinessStrategy):Boolean
  removeBizS(b:BusinessStrategy):Boolean
  businessStrategyCollection(): Set( BusinessStrategy ) = self.businessStrategy 
  isEqualTo(p:Pattern):Boolean = 
	((self.name = p.name) and 
	(self.GMBB.isEqualTo(p.GMBB)) and 
	(self.businessStrategy->forAll(b1|p.businessStrategy->exists(b2|b2.isEqualTo(b1)))) and
	(p.businessStrategy->forAll(b1|self.businessStrategy->exists(b2|b2.isEqualTo(b1)))))
  DownPatternSet(s:Set(Pattern)):Set(Pattern) = 
	if s->includesAll(s.GMBB.intention.patternDef->asSet())
	then s
	else DownPatternSet(s->union(s.GMBB.intention.patternDef->asSet()))
	endif
  DefiningPatternSet():Set(Pattern) = 
	if self.GMBB.intention.patternDef->asSet()->size()>0
	then DownPatternSet(self.GMBB.intention.patternDef->asSet())
	else null
	endif

end

class GoalModelBB
attributes
  name : String
operations
  leafCollection(): Set(Intention) = self.intention->select(i|i.leaf)
  mainGoal(): Intention = self.intention->select(i|i.mainGoal)->asSequence()->at(1)
  isEqualTo(g:GoalModelBB) : Boolean = 
  	((self.name = g.name) and 
	(self.intention->forAll(i1|g.intention->exists(i2|i2.isEqualTo(i1)))) and 
	(g.intention->forAll(i1|self.intention->exists(i2|i2.isEqualTo(i1)))) and
	(self.EL->forAll(e1|g.EL->exists(e2|e2.isEqualTo(e1)))) and 
	(g.EL->forAll(e1|self.EL->exists(e2|e2.isEqualTo(e1)))))
end 

class Intention
attributes
  name : String
  leaf : Boolean
  mainGoal : Boolean
operations
  isEqualTo(i:Intention) : Boolean = 
	(self.name = i.name and
	self.mainGoal = i.mainGoal and
	self.leaf = i.leaf)
  UpIntentionSet(s:Set(Intention)):Set(Intention) = 
	if s ->includesAll(s.ELf.toLink()->asSet())
	then s
	else UpIntentionSet(s->union(s.ELf.toLink()->asSet()))
       endif
  UpIntentionSetFromSelf():Set(Intention) = UpIntentionSet(Set{self})
  DownIntentionSet(s:Set(Intention)):Set(Intention) = 
	if s ->includesAll(s.ELt.fromLink()->asSet())
	then s
	else DownIntentionSet(s->union(s.ELt.fromLink()->asSet()))
       endif
  DownIntentionSetFromSelf():Set(Intention) = DownIntentionSet (Set{self})

end 

class ElementLink
attributes
  name : String
operations
  toLink(): Intention = self.toLinks
  fromLink(): Intention = self.fromLinks
  isEqualTo(e: ElementLink) : Boolean = 
	(self.name = e.name and
	self.toLinks = e.toLinks and 
	self.fromLinks = e.fromLinks)
  linkType(): String
  weight():Integer
end

class BusinessStrategy
attributes
  name : String
operations
  isEqualTo(b:BusinessStrategy) : Boolean = 
	(self.name = b.name and
	self.BPBB.isEqualTo(b.BPBB) and 
	self.evaluationStrategy.isEqualTo(b.evaluationStrategy))
end

class EvaluationStrategy
attributes
  name : String
operations
  isEqualTo(s:EvaluationStrategy) : Boolean = 
  	(self.name = s.name)

end 

class BusinessProcessBB
attributes
  name : String
operations
  isEqualTo(b:BusinessProcessBB) : Boolean = 
	(self.name = b.name and
	(self.PE->forAll(pe1|b.PE->exists(pe2|pe2.isEqualTo(pe1)))) and 
	(b.PE->forAll(pe1|self.PE->exists(pe2|pe2.isEqualTo(pe1)))))
end 

class ProcessElement
attributes
  name : String
operations
  isEqualTo(pe:ProcessElement) : Boolean = 
  	(self.name = pe.name and
	self.realized.isEqualTo(pe.realized))
end

------------------
-- ASSOCIATIONS --
------------------

aggregation hasPattern between
  PF[1] role family
  Pattern[0..*] role pattern
end

aggregation hasGMBB between
  Pattern[1] role pattern
  GoalModelBB[1] role GMBB
end

aggregation hasIntention between
  GoalModelBB[1] role GMBB
  Intention[0..*] role intention
end

aggregation hasBizStrategy between
  Pattern[1] role pattern
  BusinessStrategy[1..*] role businessStrategy
end

aggregation hasEvalStrategy between
  BusinessStrategy[1] role businessStrategy 
  EvaluationStrategy[1] role evaluationStrategy
end

aggregation hasBPBB between
  BusinessStrategy[1] role businessStrategy 
  BusinessProcessBB[1] role BPBB
end

aggregation hasPE between
  BusinessProcessBB[1] role BPBB
  ProcessElement[1..*] role PE
end

aggregation hasElementLink between
  GoalModelBB[1] role GMBB
  ElementLink[0..*] role EL
end

association realized between
  Intention[0..1] role realized
  ProcessElement[0..*] role realizingElement
end

association define between
  Intention[0..*] role refined
  Pattern[0..1] role patternDef
end

association linkTo between
  ElementLink[0..*] role ELt
  Intention[1] role toLinks 
end

association linkFrom between
  ElementLink[0..*] role ELf
  Intention[1] role fromLinks 
end 

-----------------
-- CONSTRAINTS --
-----------------


constraints

---------
-- PF --
---------
context PF

inv UniquePFName:
PF.allInstances()->isUnique(name)

inv UniquePatternNameInPF: 
self.pattern->isUnique(name)

inv UniquePatternMainGoalInPF: 
self.pattern->isUnique(GMBB.mainGoal().name)

inv UniqueEvalStrategyInPF:
self.pattern.businessStrategy.evaluationStrategy->isUnique(name)

--inv AllPossibleRefiningLeafConnected2:
--self.pattern.GMBB.intention->forAll(i|i.leaf implies self.pattern->forAll(p|(i.name = p.GMBB.mainGoal().name and i.GMBB.pattern<>p) implies i.patternDef = p))



-------------
---PATTERN---
-------------
context Pattern

inv UniqueBusinessStrategyNameInPattern:
self.businessStrategy->isUnique(name)

inv OnlyLeavesRefine: 
self.refined->forAll(i|i.leaf)

inv CorrectLeafMainGoalRefinement: 
self.refined->forAll(i|i.name = self.GMBB.mainGoal().name)

inv NoLoop1Level:
self.GMBB.intention.patternDef->excludes(self)

inv NoOrphanPattern:
Pattern.allInstances()->one(p| p.refined->size()=0)

inv NoCircularDefiningPatternExist:
self.DefiningPatternSet()->excludes(self)


context Pattern:: businessStrategyCollection(): Set( BusinessStrategy )
post businessStrategyCollectionisDone: result = self.businessStrategy

context Pattern:: replaceGMBB(g:GoalModelBB):Boolean 
post addGMBBisDone: result = (self.GMBB=g)

context Pattern:: addBizS(b:BusinessStrategy):Boolean 
post addBizSisDone: result = (self.businessStrategy = self.businessStrategy@pre->including(b))

context Pattern:: removeBizS(b:BusinessStrategy):Boolean 
post removeBizSisDone: result = (self.businessStrategy = self.businessStrategy@pre->excluding(b))
  
  
-----------------
--GOAL MODEL BUILDING BLOCK--
-----------------
context GoalModelBB

inv UniqueIntenionNameInGMBB:
self.intention->isUnique(name)

inv UniqueElementLinkNameInGMBB:
self.EL->isUnique(name)

inv JustOneMainGoal:
self.intention->one(i|i.mainGoal)


context GoalModelBB:: leafCollection(): Set(Intention) 
post leafCollectionisDone: result = self.intention->select(i|i.leaf)

--context GoalModelBB:: mainGoal(): Intention 
--post mainGoalisDone: self.intention->forAll(i|i.mainGoal implies result = i) 


-------------
--INTENTION--
-------------
context Intention

inv LeavesBeingRefined:
self.patternDef<>null implies self.leaf

inv ElementsAreIncludedInRelatedBSTs:
self.GMBB.pattern.businessStrategy.BPBB.PE -> includesAll(self.realizingElement)

inv EitherMainGoalOrLeaf:
not (mainGoal and leaf)
--it possible for intention to be neither mainGoal or Leaf 

inv LeavesAreConnected:
self.leaf implies self.GMBB.EL->exists(e|e.fromLink()=self)

inv MainGoalsAreConnected:
self.mainGoal implies self.GMBB.EL->exists(e|e.toLink()=self)

inv MiddleGoalAreConnected:
(not self.mainGoal and not self.leaf) implies self.GMBB.EL->exists(e1, e2|e1.toLink()= self and e2.fromLink() = self)

inv AllPossibleRefiningLeafConnected:
self.leaf implies Pattern.allInstances()->forAll(p|(self.name = p.GMBB.mainGoal().name and self.GMBB.pattern<>p and self.GMBB.pattern.family.name=p.family.name) implies self.patternDef = p)

inv NoMiddleIntentionPossibleRefinement:
Pattern.allInstances()->exists(p|self.name = p.GMBB.mainGoal().name) implies (self.leaf or self.mainGoal)

inv NoDanglingMiddleIntention:
not (self.leaf or self.mainGoal) implies (DownIntentionSetFromSelf()-> exists(i|i.leaf))

inv LeavesHaveOneMainGoal:
self.leaf implies UpIntentionSetFromSelf()->one(i|i.mainGoal)

inv MainGoalsHaveAtLeastOneLeaf:
self.mainGoal implies DownIntentionSetFromSelf()->exists(i|i.leaf)


----------------
--ELEMENT LINK--
----------------
context ElementLink

inv DifferentSourceDestination:
self.toLinks<>self.fromLinks


---------------------
--BUSINESS STRATEGY--
---------------------
context BusinessStrategy


------------
--EVALUATION STRATEGY--
------------
--context EvaluationStrategy

--inv UniqueEvalStrategyName:
--EvaluationStrategy.allInstances()->isUnique(name)

-----------------------------
--BUSINESS PROCESS BUILDING BLOCK--
-----------------------------
context BusinessProcessBB

inv UniqueProcessElementNameInBPBB:
self.PE->isUnique(name)


-----------------------------
--PROCESS ELEMENT--
-----------------------------