aboutsummaryrefslogtreecommitdiffstats
blob: debcd0d3cd62151b87d66ddb29e7c6409fbeaae9 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
/*
 * Copyright (c) 2018 Christian W. Damus and others.
 * 
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *   Christian W. Damus - Initial API and implementation
 *   
 */

import 'http://www.eclipse.org/uml2/5.0.0/UML'

package UML

context Element

-- A helper operation that reports a problem as error severity instead of warning.
def: asError(ok: Boolean): Boolean = if ok then ok else null endif

context Message

--
-- The ends of a message that are not Gates are all owned by the same
-- Interaction or InteractionOperand.
--
inv crosses_no_boundaries('Message crosses an interaction operand boundary.'):
	let ends = Set{sendEvent, receiveEvent}->excluding(null)->reject(oclIsKindOf(Gate)) in
	asError(ends->notEmpty() implies ends.owner->asSet()->size() = 1)


context ExecutionSpecification

--
-- The start and finish events if an execution specification are both owned
-- by the same Interaction or InteractionOperand.
--
inv crosses_no_boundaries('Execution specification crosses an interaction operand boundary.'):
	let events = Set{start, finish}->excluding(null) in
	asError(events->notEmpty() implies events.owner->asSet()->size() = 1)

endpackage