AlloyInEcore

package requirementsmodel: tol= 'eu.modelwriter.examples.requirementsmodels'
{
	public class Requirement [4]  
	{
		property req: Requirement [*] {transitive, irreflexive, antisymmetric};
		property refines: Requirement [*] {transitive, irreflexive, antisymmetric};
		property contains: Requirement [*] {transitive, irreflexive, antisymmetric};
		property conflicts: Requirement [*] {irreflexive, symmetric};
		property equals: Requirement [*] {equivalence};
		property partially_refines: Requirement [*] {transitive, irreflexive, antisymmetric};
		
		attribute name: String [1];
		
		invariant: all a, b: Requirement | (a != b) implies (a.name != b.name); 
		invariant: ("Daniel" + "Sarfraz" + "Emina" + "Eunsuk") in EString ;
	}
	
	public class TestCases extends Requirement{}
	
	-- No intersection
	invariant: no (req + ~req) & (refines + ~refines);
	invariant: no (contains + ~contains) & (equals + ~equals);
	invariant: no (conflicts + ~conflicts) & (partially_refines + ~partially_refines);
	invariant: no (req + ~req + refines + ~refines) & (contains + ~contains + equals + ~equals);
	invariant: no (req + ~req + refines + ~refines + contains + ~contains + equals + ~equals) 
	                        & (conflicts + ~conflicts + partially_refines + ~partially_refines);


	-- Inferring new relations
	invariant: req.refines in req;
	invariant: req.contains in req;
	invariant: req.conflicts in conflicts;
	invariant: req.equals in req;
	
	invariant: refines.req in req;
	invariant: refines.contains in refines;
	invariant: refines.partially_refines in partially_refines;
	invariant: refines.conflicts in conflicts;
	invariant: refines.equals in refines;
	
	invariant: contains.req in req;
	invariant: contains.refines in refines;
	invariant: contains.partially_refines in partially_refines;
	invariant: contains.conflicts in conflicts;
	invariant: contains.equals in contains;
	
	invariant: partially_refines.equals in partially_refines;
	
	invariant: conflicts.equals in conflicts;
	
	invariant: equals.req in req;
	invariant: equals.refines in refines;
	invariant: equals.contains in contains;
	invariant: equals.conflicts in conflicts;
	invariant: equals.partially_refines in partially_refines;	
}