AlloyInEcore

import Ecore : "http://www.eclipse.org/emf/2002/Ecore";

package ArchitectureMetamodel : arch = "eu.modelwriter.demonstrations.metamodels.architecture"
{
    public class one ArchitecturalModel
    {
        property one elements : ArchitecturalElement[*] { composes };
        
        model property leaves : Component[*];        
        invariant leaves: Component - Component.^~subComponents in ArchitecturalModel.leaves;
        
        invariant : ArchitecturalModel.elements not in ArchitecturalModel.leaves;
        
        model property one root: Component[1];
        invariant root: Component in ArchitecturalModel.root.*subComponents;
        
    }
    abstract class ArchitecturalElement [9]
    {
        attribute identifier : Integer[1] {id}; 
		invariant : all disj a, b: ArchitecturalElement | a.identifier != b.identifier;
        //invariant : some a:ArchitecturalElement | 
                             all b: ArchitecturalElement | a.identifier > b.identifier;
        attribute name : String[1];
        invariant : all c: Component | some c.subComponents implies #c.subComponents = 2;
    }
    class Component extends ArchitecturalElement
    {
        property subComponents : Component[*] { composes };
        ghost attribute description: String = 'Default Description';      
        
        model attribute isLeaf: Boolean { derived };      
		invariant isLeaf: all c: Component | no c.subComponents and 
		                                              no c.~root implies c.isLeaf = True;
		//invariant isLeaf': ArchitecturalModel.root.isLeaf = False;
    }
}