Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module EA_Model
- open world_structure[World]
- open ontological_properties[World]
- open util/relation
- open util/ternary
- open util/boolean
- abstract sig Object {}
- abstract sig cItem extends Object {}
- sig kSoftwareTool extends cItem {}
- abstract sig cArtifact extends cItem {}
- sig kSourceCode extends cArtifact {}
- sig kDocument extends cArtifact {}
- sig kDiagram extends cArtifact {}
- sig kChange extends Object {}
- sig kPerson extends Object {}
- sig kProject extends Object{}
- sig coBranch extends Object{}
- sig coRepository extends Object{}
- abstract sig Property {}
- sig modeVersion extends Property{}
- sig modeConfiguration extends modeVersion{}
- sig modeAtomicVersion extends modeVersion{}
- sig relatorChangeRequest extends Property{}
- sig relatorVerification extends Property{}
- sig relatorCheckIn extends Property{}
- sig relatorCheckOut extends Property{}
- sig relatorConfigurationSelection extends Property{}
- sig relatorModification extends Property{}
- sig relatorRequestEvaluation extends Property{}
- sig relatorMarkup extends Property{}
- sig DataType {}
- sig String_ {}
- abstract sig World {
- exists: some Object+Property,
- Artifact: set exists:>cArtifact,
- AtomicCI: set exists:>cItem,
- AtomicVersion: set exists:>modeAtomicVersion,
- Baseline: set exists:>modeConfiguration,
- Branch: set exists:>coBranch,
- Change: set exists:>kChange,
- ChangeRequest: set exists:>relatorChangeRequest,
- CheckedOutVersion: set exists:>modeVersion,
- CheckIn: set exists:>relatorCheckIn,
- CheckOut: set exists:>relatorCheckOut,
- CompositeCI: set exists:>cItem,
- Configuration: set exists:>modeConfiguration,
- ConfigurationItem: set exists:>cItem,
- ConfigurationManager: set exists:>Object,
- ConfigurationSelection: set exists:>relatorConfigurationSelection,
- Developer: set exists:>kPerson,
- Diagram: set exists:>kDiagram,
- Document: set exists:>kDocument,
- EvaluatedRequest: set exists:>relatorChangeRequest,
- Evaluator: set exists:>kPerson,
- ImplementedChange: set exists:>kChange,
- Item: set exists:>cItem,
- Markup: set exists:>relatorMarkup,
- Modification: set exists:>relatorModification,
- ModifiedVersion: set exists:>modeVersion,
- OnGoingChange: set exists:>kChange,
- Person: set exists:>kPerson,
- Project: set exists:>kProject,
- RegisteredModification: set exists:>relatorModification,
- Repository: set exists:>coRepository,
- Requester: set exists:>kPerson,
- RequestEvaluation: set exists:>relatorRequestEvaluation,
- Revision: set exists:>modeVersion,
- SoftwareTool: set exists:>kSoftwareTool,
- SourceCode: set exists:>kSourceCode,
- Variant: set exists:>modeVersion,
- Verification: set exists:>relatorVerification,
- VerifiedChange: set exists:>kChange,
- Verifyer: set exists:>kPerson,
- Version: set exists:>modeVersion,
- VersionSubmittedForChange: set exists:>modeVersion,
- Association: set Project one -> some Repository,
- Characterization1: set Configuration some -> one CompositeCI,
- Characterization2: set Version some -> one ConfigurationItem,
- Characterization: set AtomicVersion some -> one AtomicCI,
- ComponentOf1: set Configuration lone -> some Version,
- ComponentOf: set CompositeCI lone -> some ConfigurationItem,
- Mediation10: set CheckOut one -> some CheckedOutVersion,
- Mediation11: set ConfigurationSelection one -> some ConfigurationItem,
- Mediation12: set Markup some -> some ConfigurationManager,
- Mediation13: set ConfigurationSelection some -> one ConfigurationManager,
- Mediation14: set Modification set -> one Developer,
- Mediation15: set RequestEvaluation one -> one EvaluatedRequest,
- Mediation16: set RequestEvaluation some -> one Evaluator,
- Mediation17: set Modification one -> one ModifiedVersion,
- Mediation18: set Verification one -> some VerifiedChange,
- Mediation19: set Verification some -> some Verifyer,
- Mediation1: set ChangeRequest some -> some Change,
- Mediation2: set ChangeRequest some -> one Requester,
- Mediation3: set ChangeRequest some -> some VersionSubmittedForChange,
- Mediation4: set CheckIn one -> some RegisteredModification,
- Mediation5: set CheckIn one -> one ImplementedChange,
- Mediation6: set CheckIn set -> one Developer,
- Mediation7: set CheckIn one -> some Version,
- Mediation8: set CheckOut one -> one OnGoingChange,
- Mediation9: set CheckOut set -> one Developer,
- Mediation: set Markup one -> one Baseline,
- MemberOf: set Branch one -> some Version,
- SubCollectionOf: set Repository one -> some Branch
- }{
- Artifact = Diagram+Document+SourceCode
- Item = SoftwareTool+AtomicCI+Diagram+Artifact+Document+CompositeCI+ConfigurationItem+SourceCode
- ConfigurationItem = AtomicCI+CompositeCI
- all x: CompositeCI | # (x.ComponentOf) >= 2
- all x: Configuration | # (x.ComponentOf1) >= 2
- disj[Repository,Document,Change,Person,Diagram,SourceCode,SoftwareTool,Project,Branch]
- exists:>Object in Repository+Artifact+Document+ModifiedVersion+Change+Person+Diagram+Item+SourceCode+Developer+Baseline+EvaluatedRequest+CompositeCI+RegisteredModification+AtomicCI+CheckedOutVersion+SoftwareTool+ConfigurationManager+Project+Requester+VerifiedChange+VersionSubmittedForChange+OnGoingChange+Verifyer+Branch+Evaluator+ConfigurationItem+ImplementedChange
- exists:>Property in Version+Configuration+Modification+Verification+ConfigurationSelection+Variant+CheckIn+Markup+ChangeRequest+RequestEvaluation+CheckOut+Revision+AtomicVersion
- disj[Item,Project+Repository+Person+Branch+Change]
- disj[Project,Repository+Item+Person+Branch+Change]
- disj[Branch,Project+Repository+Item+Person+Change]
- disj[Change,Project+Repository+Item+Person+Branch]
- disj[Person,Project+Repository+Item+Branch+Change]
- disj[Repository,Project+Item+Person+Branch+Change]
- disj[ConfigurationSelection,Modification+Version+Markup+RequestEvaluation+CheckIn+ChangeRequest+Verification+CheckOut]
- disj[CheckOut,Modification+Version+Markup+RequestEvaluation+CheckIn+ChangeRequest+Verification+ConfigurationSelection]
- disj[CheckIn,Modification+Version+Markup+RequestEvaluation+ChangeRequest+Verification+ConfigurationSelection+CheckOut]
- disj[RequestEvaluation,Modification+Version+Markup+CheckIn+ChangeRequest+Verification+ConfigurationSelection+CheckOut]
- disj[Verification,Modification+Version+Markup+RequestEvaluation+CheckIn+ChangeRequest+ConfigurationSelection+CheckOut]
- disj[Markup,Modification+Version+RequestEvaluation+CheckIn+ChangeRequest+Verification+ConfigurationSelection+CheckOut]
- disj[Version,Modification+Markup+RequestEvaluation+CheckIn+ChangeRequest+Verification+ConfigurationSelection+CheckOut]
- disj[ChangeRequest,Modification+Version+Markup+RequestEvaluation+CheckIn+Verification+ConfigurationSelection+CheckOut]
- disj[Modification,Version+Markup+RequestEvaluation+CheckIn+ChangeRequest+Verification+ConfigurationSelection+CheckOut]
- }
- fact additionalFacts {
- continuous_existence[exists]
- elements_existence[Object+Property,exists]
- }
- fact weakSupplementationConstraint {
- all w: World | all x: w.Repository | # (x.(w.SubCollectionOf)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.RequestEvaluation | # (x.(w.Mediation16)+x.(w.Mediation15)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.CheckOut | # (x.(w.Mediation8)+x.(w.Mediation10)+x.(w.Mediation9)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.Modification | # (x.(w.Mediation14)+x.(w.Mediation17)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.Markup | # (x.(w.Mediation12)+x.(w.Mediation)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.CheckIn | # (x.(w.Mediation4)+x.(w.Mediation5)+x.(w.Mediation6)+x.(w.Mediation7)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.ChangeRequest | # (x.(w.Mediation3)+x.(w.Mediation2)+x.(w.Mediation1)) >= 2
- }
- fact weakSupplementationConstraint {
- all w: World | all x: w.Branch | # (x.(w.MemberOf)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.Verification | # (x.(w.Mediation18)+x.(w.Mediation19)) >= 2
- }
- fact relatorConstraint {
- all w: World | all x: w.ConfigurationSelection | # (x.(w.Mediation13)+x.(w.Mediation11)) >= 2
- }
- fact acyclicMeronymic {
- all w: World | acyclic[w.ComponentOf1,w.Configuration]
- }
- fact acyclicMeronymic {
- all w: World | acyclic[w.ComponentOf,w.CompositeCI]
- }
- fact acyclicMeronymic {
- all w: World | acyclic[w.SubCollectionOf,w.Repository]
- }
- fact acyclicMeronymic {
- all w: World | acyclic[w.MemberOf,w.Branch]
- }
- fact acyclicCharacterization {
- all w: World | acyclic[w.Characterization2,w.Version]
- }
- fact acyclicCharacterization {
- all w: World | acyclic[w.Characterization1,w.Configuration]
- }
- fact acyclicCharacterization {
- all w: World | acyclic[w.Characterization,w.AtomicVersion]
- }
- fact rigidity {
- rigidity[Repository,Object,exists]
- }
- fact rigidity {
- rigidity[Version,Property,exists]
- }
- fact rigidity {
- rigidity[Configuration,Property,exists]
- }
- fact rigidity {
- rigidity[RequestEvaluation,Property,exists]
- }
- fact rigidity {
- rigidity[CheckIn,Property,exists]
- }
- fact rigidity {
- rigidity[Artifact,Object,exists]
- }
- fact rigidity {
- rigidity[Person,Object,exists]
- }
- fact rigidity {
- rigidity[ChangeRequest,Property,exists]
- }
- fact rigidity {
- rigidity[Document,Object,exists]
- }
- fact rigidity {
- rigidity[Branch,Object,exists]
- }
- fact rigidity {
- rigidity[CheckOut,Property,exists]
- }
- fact rigidity {
- rigidity[Revision,Property,exists]
- }
- fact rigidity {
- rigidity[Project,Object,exists]
- }
- fact rigidity {
- rigidity[SoftwareTool,Object,exists]
- }
- fact rigidity {
- rigidity[Variant,Property,exists]
- }
- fact rigidity {
- rigidity[Modification,Property,exists]
- }
- fact rigidity {
- rigidity[Diagram,Object,exists]
- }
- fact rigidity {
- rigidity[Markup,Property,exists]
- }
- fact rigidity {
- rigidity[Item,Object,exists]
- }
- fact rigidity {
- rigidity[Verification,Property,exists]
- }
- fact rigidity {
- rigidity[ConfigurationSelection,Property,exists]
- }
- fact rigidity {
- rigidity[AtomicVersion,Property,exists]
- }
- fact rigidity {
- rigidity[Change,Object,exists]
- }
- fact rigidity {
- rigidity[SourceCode,Object,exists]
- }
- fact generalization {
- Variant in Version
- }
- fact generalization {
- Developer in Person
- }
- fact generalization {
- ConfigurationManager in Person
- }
- fact generalization {
- VerifiedChange in ImplementedChange
- }
- fact generalization {
- Document in Artifact
- }
- fact generalization {
- ConfigurationItem in Item
- }
- fact generalization {
- Verifyer in ConfigurationManager
- }
- fact generalization {
- Evaluator in Person
- }
- fact generalization {
- AtomicVersion in Version
- }
- fact generalization {
- OnGoingChange in Change
- }
- fact generalization {
- Configuration in Version
- }
- fact generalization {
- Diagram in Artifact
- }
- fact generalization {
- Artifact in Item
- }
- fact generalization {
- SoftwareTool in Item
- }
- fact generalization {
- Revision in Version
- }
- fact generalization {
- Baseline in Configuration
- }
- fact generalization {
- AtomicCI in ConfigurationItem
- }
- fact generalization {
- Verifyer in Person
- }
- fact generalization {
- VersionSubmittedForChange in Version
- }
- fact generalization {
- EvaluatedRequest in ChangeRequest
- }
- fact generalization {
- SourceCode in Artifact
- }
- fact generalization {
- CompositeCI in ConfigurationItem
- }
- fact generalization {
- Evaluator in ConfigurationManager
- }
- fact generalization {
- Requester in Person
- }
- fact generalization {
- ModifiedVersion in Version
- }
- fact generalization {
- CheckedOutVersion in Version
- }
- fact generalization {
- RegisteredModification in Modification
- }
- fact generalization {
- ImplementedChange in Change
- }
- fun visible : World -> univ {
- exists
- }
- fact associationProperties {
- immutable_target[RequestEvaluation,Mediation15]
- immutable_target[Verification,Mediation19]
- immutable_target[Markup,Mediation12]
- immutable_target[CheckIn,Mediation7]
- }
- pred story [Mary:one Object+Property,Fred:one Object+Property,Thomas:one Object+Property,John:one Object+Property,Diagram1:one Object+Property,Document1:one Object+Property,SourceCode1:one Object+Property,ConfigSelection:one Object+Property,World0:one World]{
- Mary in World0.exists
- Mary in World0.Developer
- Fred in World0.exists
- Fred in World0.Developer
- Thomas in World0.exists
- Thomas in World0.Developer
- John in World0.exists
- John in World0.Developer
- Diagram1 in World.Diagram
- Diagram1 in World0.exists
- Document1 in World.Document
- Document1 in World0.exists
- SourceCode1 in World.SourceCode
- SourceCode1 in World0.exists
- ConfigSelection in World.ConfigurationSelection
- ConfigSelection in World0.exists
- disj[Mary,Fred,Thomas,John]
- World.Person in Mary+Fred+Thomas+John
- }
- //Associação existe nesse mundo
- /*pred direct_rel_in_w[x1,x2:Object+Property, w:World]{
- some f:World$.subfields |
- x1 in w.(f.value)[x2]
- or
- x2 in w.(f.value)[x1]
- }*/
- pred direct_rel_in_w[x1,x2:Object+Property, w:World]{
- some (x1->x2 + x2->x1)
- & ( w.Association +
- w.Characterization1 +
- w.Characterization2 +
- w.Characterization+
- w.Mediation10 +
- w.Mediation11 +
- w.Mediation12 +
- w.Mediation13 +
- w.Mediation14 +
- w.Mediation15 +
- w.Mediation16 +
- w.Mediation17 +
- w.Mediation18 +
- w.Mediation19 +
- w.Mediation1 +
- w.Mediation2 +
- w.Mediation3 +
- w.Mediation4 +
- w.Mediation5 +
- w.Mediation6 +
- w.Mediation7 +
- w.Mediation8 +
- w.Mediation9 +
- w.Mediation +
- w.MemberOf +
- w.SubCollectionOf )
- }
- pred story2 [John:one Object+Property,Mary:one Object+Property,Fred:one Object+Property,Thomas:one Object+Property,Selection1:one Object+Property,SourceCode1:one Object+Property,Doc1:one Object+Property,Diag1:one Object+Property,World0:one World,,]{
- John in World0.exists
- John in World0.Developer
- Mary in World0.exists
- Mary in World0.Developer
- Fred in World0.exists
- Fred in World0.Developer
- Thomas in World0.exists
- Thomas in World0.Developer
- Selection1 in World.ConfigurationSelection
- Selection1 in World0.exists
- direct_rel_in_w[(Selection1),(Diag1),World0]
- direct_rel_in_w[(Selection1),(Doc1),World0]
- direct_rel_in_w[(Selection1),(SourceCode1),World0]
- SourceCode1 in World.SourceCode
- SourceCode1 in World0.exists
- Doc1 in World.Document
- Doc1 in World0.exists
- Diag1 in World.Diagram
- Diag1 in World0.exists
- }
- pred story3 [World0:one World,
- World1:one World,
- World2:one World,
- World3:one World,
- Thomas:one Object+Property,
- Mary:one Object+Property,
- Fred:one Object+Property,
- John:one Object+Property,
- BakeryProcessDiagram:one Object+Property,
- DiagramVersion:one Object+Property,
- SourceDocumentation:one Object+Property,
- BakerySourcecode:one Object+Property,
- selection:one Object+Property,
- markup01:one Object+Property,
- Configuration01:one Object+Property,
- FredsChangeRequest:one Object+Property,
- diagCheckOut:one Object+Property,]{
- disj[Thomas,Mary,Fred,John]
- Thomas in World.Person
- Thomas in World0.exists
- Thomas in World1.exists
- Thomas in World2.exists
- Thomas in World3.exists
- Thomas in World0.Developer
- Thomas in World1.Developer
- Thomas in World2.Developer
- Thomas in World3.Developer
- Mary in World.Person
- Mary in World0.exists
- Mary in World1.exists
- Mary in World2.exists
- Mary in World3.exists
- Mary in World0.Developer
- Mary in World1.Developer
- Mary in World2.Developer
- Mary in World3.Developer
- Fred in World.Person
- Fred in World0.exists
- Fred in World1.exists
- Fred in World2.exists
- Fred in World3.exists
- Fred in World0.Developer
- Fred in World1.Developer
- Fred in World2.Developer
- Fred in World3.Developer
- Fred in World2.Requester
- Fred in World3.Requester
- not Fred in World0.Requester
- not Fred in World1.Requester
- John in World.Person
- John in World0.exists
- John in World1.exists
- John in World2.exists
- John in World3.exists
- John in World0.Developer
- John in World1.Developer
- John in World2.Developer
- John in World3.Developer
- BakeryProcessDiagram in World.Diagram
- BakeryProcessDiagram in World.Artifact
- BakeryProcessDiagram in World0.exists
- BakeryProcessDiagram in World1.exists
- BakeryProcessDiagram in World2.exists
- BakeryProcessDiagram in World3.exists
- DiagramVersion in World.Version
- DiagramVersion in World0.exists
- DiagramVersion in World1.exists
- DiagramVersion in World2.exists
- DiagramVersion in World3.exists
- DiagramVersion in World2.VersionSubmittedForChange
- DiagramVersion in World3.VersionSubmittedForChange
- not DiagramVersion in World1.VersionSubmittedForChange
- not DiagramVersion in World0.VersionSubmittedForChange
- SourceDocumentation in World.Artifact
- SourceDocumentation in World.Document
- SourceDocumentation in World0.exists
- SourceDocumentation in World1.exists
- SourceDocumentation in World2.exists
- SourceDocumentation in World3.exists
- BakerySourcecode in World.Artifact
- BakerySourcecode in World.SourceCode
- BakerySourcecode in World0.exists
- BakerySourcecode in World1.exists
- BakerySourcecode in World2.exists
- BakerySourcecode in World3.exists
- selection in World.ConfigurationSelection
- selection in World1.exists
- selection in World2.exists
- selection in World3.exists
- selection not in World0.exists
- markup01 in World.Markup
- markup01 in World1.exists
- markup01 in World2.exists
- markup01 in World3.exists
- markup01 not in World0.exists
- Configuration01 in World1.exists
- Configuration01 in World0.exists
- Configuration01 in World2.exists
- Configuration01 in World3.exists
- Configuration01 in World1.Baseline
- Configuration01 in World2.Baseline
- Configuration01 in World3.Baseline
- not Configuration01 in World0.Baseline
- FredsChangeRequest in World.ChangeRequest
- FredsChangeRequest in World2.exists
- FredsChangeRequest in World3.exists
- FredsChangeRequest not in World0.exists
- FredsChangeRequest not in World1.exists
- diagCheckOut in World.CheckOut
- diagCheckOut in World3.exists
- diagCheckOut not in World2.exists
- diagCheckOut not in World1.exists
- diagCheckOut not in World0.exists
- direct_rel_in_w[(FredsChangeRequest),(Fred),World2]
- direct_rel_in_w[(FredsChangeRequest),(Fred),World3]
- not direct_rel_in_w[(FredsChangeRequest),(Fred),World0]
- not direct_rel_in_w[(FredsChangeRequest),(Fred),World1]
- direct_rel_in_w[(DiagramVersion),(diagCheckOut),World3]
- not direct_rel_in_w[(DiagramVersion),(diagCheckOut),World0]
- not direct_rel_in_w[(DiagramVersion),(diagCheckOut),World1]
- not direct_rel_in_w[(DiagramVersion),(diagCheckOut),World2]
- direct_rel_in_w[(FredsChangeRequest),(DiagramVersion),World2]
- direct_rel_in_w[(FredsChangeRequest),(DiagramVersion),World3]
- not direct_rel_in_w[(FredsChangeRequest),(DiagramVersion),World1]
- not direct_rel_in_w[(FredsChangeRequest),(DiagramVersion),World0]
- direct_rel_in_w[(selection),(Thomas),World1]
- direct_rel_in_w[(selection),(Thomas),World2]
- direct_rel_in_w[(selection),(Thomas),World3]
- not direct_rel_in_w[(Thomas),(selection),World0]
- direct_rel_in_w[(BakerySourcecode),(selection),World1]
- direct_rel_in_w[(BakerySourcecode),(selection),World2]
- direct_rel_in_w[(BakerySourcecode),(selection),World3]
- not direct_rel_in_w[(BakerySourcecode),(selection),World0]
- direct_rel_in_w[(markup01),(Configuration01),World1]
- direct_rel_in_w[(markup01),(Configuration01),World2]
- direct_rel_in_w[(markup01),(Configuration01),World3]
- not direct_rel_in_w[(markup01),(Configuration01),World0]
- }
- run story3 for 14 but 4 World
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement