(cl-text Port0
(cl-comment "Port0
			[0] all ports should be typed")
(forall (p)   
		(if (cbuml:Port p)
			(exists (t)
					(buml:type p t)
				) 	 
	     )
	)	
)

(cl-text Port1
(cl-comment "Port
			[1] port is behavior type must be abstract")
(forall (p c)   
		(if (and
			(cbuml:Port p)
			(cbuml:isBehavior p form:true)
			(buml:type p c)
			)
			(cbuml:isAbstract c form:true)
	     )
	)	
)

(cl-text Port1.1
(cl-comment "Port
			[1.1] Ports is Behavior must not be connected to internal parts (stored in ownedConnectors)")
(forall (c p)   
		(if (and
				 (buml:Class c)
				 (cbuml:Port p)
				 (buml:ownedAttribute c p)
				 (cbuml:isBehavior p form:true) 
				 )
			(not (exists (co ce)
					(and
						(form:port-conn-assembly p c)
						(cbuml:ownedConnector c co)
					))
					)	 
	     )
	)
)

(cl-text Port1.2
(cl-comment "Port
			[1.2] Port is Behavior and is not conjugated, implies inheritance of the owner class from the type of the port")
(forall (c csub p)   
		(if (and
				(buml:Class c)
				(buml:Class csub)
				(cbuml:Port p)
				(buml:ownedAttribute c p)
				(cbuml:isBehavior p form:true)
				(not (cbuml:isConjugated p form:true))
				(buml:type p csub))
			(form:general-abstract c csub)
	     )
	)	
)

(cl-text Port1.3
(cl-comment "Port
			[1.3] Port is Behavior and is conjugated, implies assembly connector")
(forall (p)   
		(if (and
				(cbuml:Port p)
				(cbuml:isBehavior p form:true)
				(cbuml:isConjugated p form:true)
				)
			(exists (c)
				(form:port-conn-assembly p c)
				)	
	     )
	)	
)

(cl-text Port2
(cl-comment "Port
			[2] port is not behavior type cannot be abstract")
(forall (p c)   
		(if (and
				(buml:Class c)
				(cbuml:Port p)
				(not (cbuml:isBehavior p form:true))
				(buml:type p c))
			(not (cbuml:isAbstract c form:true))
	     )
	)	
)

(cl-text Port2.1
(cl-comment "Port
			[2.1] ports not is behavior must be direct subtype of one abstract class (one consolidated abstract class)")
(forall (p csub)   
		(if (and
			(cbuml:Port p)
			(buml:type p csub)
			(not (cbuml:isBehavior p form:true))
			)
			(exists (csup) 
				(and 
					(buml:general csub csup)
					(cbuml:isAbstract csup form:true)
					(not (cbuml:isAbstract csub form:true))
					))
	     )
	)	
)
	
(cl-text Port2.2
(cl-comment "Port
			[2.2] port not is behavior (at least one connector delegation)
			It was REMOVED from the FINAL VERSION
			because a classifier behavior can be the sole activity to send signal to a port that is not behavior or to manipulate the passive port, therefore, a delegation is not mandatory")
)
		

(cl-text Port3
(cl-comment "Port
			[3] ports in active objects must contain only reception")
(forall (c p t)   
		(if (and
				 (buml:Class c)
				 (cbuml:Port p)
				 (cbuml:isActive c form:true) 
				 (buml:ownedAttribute c p)
				 (buml:type p t))
			(exists (r) 
				(form:owned-reception-general t r))
	     )
	)
)

(cl-text Port4
(cl-comment "Port
			[4] ports in passive objects must contain operations, and not attributes")
(forall (c p t)   
		(if (and
				 (buml:Class c)
				 (cbuml:Port p)
				 (not (cbuml:isActive c form:true)) 
				 (buml:ownedAttribute c p)
				 (buml:type p t))
			(and
				(not (exists(a)
					    (form:owned-attribute-general-visible c a)))
				(exists(o)
					    (form:owned-operation-general-visible c o))		
				)
	     )
	)
)

(cl-text support
(cl-imports cbuml_support)
)