<?xml version="1.0" encoding="UTF-8"?> | |
<pivot:Model xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:pivot="http://www.eclipse.org/ocl/2015/Pivot" | |
xsi:schemaLocation="http://www.eclipse.org/ocl/2015/Pivot java://org.eclipse.ocl.pivot.PivotPackage" xmi:id="AAAAA" name="Hospital.ocl" externalURI="platform:/resource/XMLplay/model/Hospital.ocl" xmiidVersion="1"> | |
<ownedImports importedNamespace="pivot:Model Hospital.ecore.oclas#AAAAA" xmiidVersion="1"/> | |
<ownedPackages xmi:id="ecwDJ" name="hosp" URI="hosp"> | |
<ownedClasses xmi:id="FXncz" name="Hospital"> | |
<ownedInvariants xmi:id="bBKaE" name="maxPatients"> | |
<ownedSpecification xsi:type="pivot:ExpressionInOCL" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
body="self.patients->size() <= self.beds
"> | |
<ownedBody xsi:type="pivot:OperationCallExp" name="<=" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#8brvY"> | |
<ownedSource xsi:type="pivot:OperationCallExp" name="size" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#tYtCd" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#eYPCX"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="patients" type="#52UnR" referredProperty="Hospital.ecore.oclas#XFYDm"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#jQqum"/> | |
</ownedSource> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:PropertyCallExp" name="beds" type="pivot:DataType http://www.eclipse.org/emf/2002/Ecore.oclas#1EhKl" | |
referredProperty="Hospital.ecore.oclas#b9hkc"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#jQqum"/> | |
</ownedArguments> | |
</ownedBody> | |
<ownedContext xsi:type="pivot:ParameterVariable" xmi:id="jQqum" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz"/> | |
</ownedSpecification> | |
</ownedInvariants> | |
<ownedInvariants xmi:id="4r1zp" name="uniquePatientId"> | |
<ownedSpecification xsi:type="pivot:ExpressionInOCL" isRequired="false" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
body="self.patients->forAll(p1, p2 | p1 <> p2 implies p1.id <> p2.id)

"> | |
<ownedBody xsi:type="pivot:IteratorExp" name="forAll" isRequired="false" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredIteration="http://www.eclipse.org/ocl/2015/Library.oclas#YtmML"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="patients" type="#52UnR" referredProperty="Hospital.ecore.oclas#XFYDm"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#ouHq,"/> | |
</ownedSource> | |
<ownedBody xsi:type="pivot:OperationCallExp" name="implies" isRequired="false" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#cIALH"> | |
<ownedSource xsi:type="pivot:OperationCallExp" name="<>" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#X1Ovl"> | |
<ownedSource xsi:type="pivot:VariableExp" name="p1" type="pivot:Class Hospital.ecore.oclas#QZZv1" referredVariable="#2Kq28"/> | |
<ownedArguments xsi:type="pivot:VariableExp" name="p2" type="pivot:Class Hospital.ecore.oclas#QZZv1" referredVariable="#3Kq28"/> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:OperationCallExp" name="<>" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#ZmEtV"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="id" type="pivot:DataType http://www.eclipse.org/emf/2002/Ecore.oclas#1EhKl" | |
referredProperty="Hospital.ecore.oclas#DLOBC"> | |
<ownedSource xsi:type="pivot:VariableExp" name="p1" type="pivot:Class Hospital.ecore.oclas#QZZv1" referredVariable="#2Kq28"/> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:PropertyCallExp" name="id" type="pivot:DataType http://www.eclipse.org/emf/2002/Ecore.oclas#1EhKl" | |
referredProperty="Hospital.ecore.oclas#DLOBC"> | |
<ownedSource xsi:type="pivot:VariableExp" name="p2" type="pivot:Class Hospital.ecore.oclas#QZZv1" referredVariable="#3Kq28"/> | |
</ownedArguments> | |
</ownedArguments> | |
</ownedBody> | |
<ownedIterators xsi:type="pivot:IteratorVariable" xmi:id="2Kq28" name="p1" type="pivot:Class Hospital.ecore.oclas#QZZv1" representedParameter="http://www.eclipse.org/ocl/2015/Library.oclas#//@ownedPackages.0/@ownedClasses.25/@ownedOperations.34/@ownedIterators.0"/> | |
<ownedIterators xsi:type="pivot:IteratorVariable" xmi:id="3Kq28" name="p2" type="pivot:Class Hospital.ecore.oclas#QZZv1" representedParameter="http://www.eclipse.org/ocl/2015/Library.oclas#//@ownedPackages.0/@ownedClasses.25/@ownedOperations.34/@ownedIterators.1"/> | |
</ownedBody> | |
<ownedContext xsi:type="pivot:ParameterVariable" xmi:id="ouHq," name="self" type="pivot:Class Hospital.ecore.oclas#FXncz"/> | |
</ownedSpecification> | |
</ownedInvariants> | |
<ownedOperations xmi:id="GLEKL" name="admitPatient" isRequired="false" type="pivot:VoidType http://www.eclipse.org/ocl/2015/Library.oclas#7u3MH"> | |
<ownedParameters xmi:id="JBbKJ" name="p" isRequired="false" type="pivot:Class Hospital.ecore.oclas#QZZv1"/> | |
<ownedPostconditions xmi:id=",ZJmO"> | |
<ownedSpecification xsi:type="pivot:ExpressionInOCL" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
body="self.patients = self.patients@pre->including(p)

"> | |
<ownedBody xsi:type="pivot:OperationCallExp" name="=" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#eR9Jh"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="patients" type="#52UnR" referredProperty="Hospital.ecore.oclas#XFYDm"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#ntull"/> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:OperationCallExp" name="including" type="#32UnR" referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#eutuy"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="patients" type="#52UnR" isPre="true" referredProperty="Hospital.ecore.oclas#XFYDm"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#ntull"/> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:VariableExp" name="p" isRequired="false" type="pivot:Class Hospital.ecore.oclas#QZZv1" | |
referredVariable="#QeqPx"/> | |
</ownedArguments> | |
</ownedBody> | |
<ownedContext xsi:type="pivot:ParameterVariable" xmi:id="ntull" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz"/> | |
<ownedParameters xsi:type="pivot:ParameterVariable" xmi:id="QeqPx" name="p" isRequired="false" type="pivot:Class Hospital.ecore.oclas#QZZv1" | |
representedParameter="#JBbKJ"/> | |
<ownedResult xsi:type="pivot:ParameterVariable" name="result" isRequired="false" type="pivot:VoidType http://www.eclipse.org/ocl/2015/Library.oclas#7u3MH"/> | |
</ownedSpecification> | |
</ownedPostconditions> | |
<ownedPreconditions xmi:id="8ZaCZ"> | |
<ownedSpecification xsi:type="pivot:ExpressionInOCL" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
body="self.beds > 0
"> | |
<ownedBody xsi:type="pivot:OperationCallExp" name=">" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#XEMMs" | |
referredOperation="http://www.eclipse.org/ocl/2015/Library.oclas#5+qvY"> | |
<ownedSource xsi:type="pivot:PropertyCallExp" name="beds" type="pivot:DataType http://www.eclipse.org/emf/2002/Ecore.oclas#1EhKl" | |
referredProperty="Hospital.ecore.oclas#b9hkc"> | |
<ownedSource xsi:type="pivot:VariableExp" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz" referredVariable="#MNM4p"/> | |
</ownedSource> | |
<ownedArguments xsi:type="pivot:IntegerLiteralExp" type="pivot:PrimitiveType http://www.eclipse.org/ocl/2015/Library.oclas#tYtCd" | |
integerSymbol="0"/> | |
</ownedBody> | |
<ownedContext xsi:type="pivot:ParameterVariable" xmi:id="MNM4p" name="self" type="pivot:Class Hospital.ecore.oclas#FXncz"/> | |
<ownedParameters xsi:type="pivot:ParameterVariable" name="p" isRequired="false" type="pivot:Class Hospital.ecore.oclas#QZZv1" | |
representedParameter="#JBbKJ"/> | |
</ownedSpecification> | |
</ownedPreconditions> | |
</ownedOperations> | |
</ownedClasses> | |
</ownedPackages> | |
<ownedPackages name="$$" URI="http://www.eclipse.org/ocl/2015/Orphanage" nsPrefix="orphanage"> | |
<ownedClasses xsi:type="pivot:OrderedSetType" xmi:id="52UnR" name="OrderedSet" superClasses="#te3yy #RJyXs" isNullFree="true" lower="1"> | |
<ownedBindings> | |
<ownedSubstitutions actual="pivot:Class Hospital.ecore.oclas#QZZv1" formal="http://www.eclipse.org/ocl/2015/Library.oclas#53+C2"/> | |
</ownedBindings> | |
</ownedClasses> | |
<ownedClasses xsi:type="pivot:OrderedSetType" xmi:id="32UnR" name="OrderedSet" superClasses="#te3yy #RJyXs"> | |
<ownedBindings> | |
<ownedSubstitutions actual="pivot:Class Hospital.ecore.oclas#QZZv1" formal="http://www.eclipse.org/ocl/2015/Library.oclas#53+C2"/> | |
</ownedBindings> | |
</ownedClasses> | |
<ownedClasses xsi:type="pivot:CollectionType" xmi:id="te3yy" name="OrderedCollection" superClasses="#gOCc8"> | |
<ownedBindings> | |
<ownedSubstitutions actual="pivot:Class Hospital.ecore.oclas#QZZv1" formal="http://www.eclipse.org/ocl/2015/Library.oclas#feFHs"/> | |
</ownedBindings> | |
</ownedClasses> | |
<ownedClasses xsi:type="pivot:CollectionType" xmi:id="RJyXs" name="UniqueCollection" superClasses="#gOCc8"> | |
<ownedBindings> | |
<ownedSubstitutions actual="pivot:Class Hospital.ecore.oclas#QZZv1" formal="http://www.eclipse.org/ocl/2015/Library.oclas#jdfjE"/> | |
</ownedBindings> | |
</ownedClasses> | |
<ownedClasses xsi:type="pivot:CollectionType" xmi:id="gOCc8" name="Collection" superClasses="http://www.eclipse.org/ocl/2015/Library.oclas#jbMkR"> | |
<ownedBindings> | |
<ownedSubstitutions actual="pivot:Class Hospital.ecore.oclas#QZZv1" formal="http://www.eclipse.org/ocl/2015/Library.oclas#qs59R"/> | |
</ownedBindings> | |
</ownedClasses> | |
</ownedPackages> | |
</pivot:Model> |