cmo.als

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