Skip to main content
aboutsummaryrefslogtreecommitdiffstats
blob: 633ac62b559b66b0be1d554b2fd43dfc90030478 (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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
/*
 * 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 2.0
 * which accompanies this distribution, and is available at
 * https://www.eclipse.org/legal/epl-2.0/
 *
 * SPDX-License-Identifier: EPL-2.0
 *
 * 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

-- Helper to render collections of strings as lists 
def: asString(list : Collection(String)) : String =
	list->iterate(i; l : String = '' |
		i + (if l.size() > 0 then ', ' else '' endif) + l)

-- Helper to put single quotes are strings in a collection 
def: quote(list : Collection(String)) : Sequence(String) =
	list->collect(i | '\'' + i + '\'')->asSequence()

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)

context CombinedFragment

--
-- An combined fragment covers all of the lifelines that are covered by the
-- fragments of its operands.
--
inv lifeline_coverage:
	let uncovered = operand.fragment.covered->asSet()->excludingAll(self.covered)->sortedBy(name) in
	Tuple {
		status = uncovered->isEmpty(),
		message = if uncovered->size() = 1 then
				'Lifeline \'' + uncovered.name->first() + '\' not covered that is covered by fragments of the operands.'
			else
				'Lifelines ' + asString(quote(uncovered.name)) + ' not covered that are covered by fragments of the operands.'
			endif
	}
		
context InteractionOperand

--
-- An interaction operand covers all of the lifelines that are covered by the
-- fragments that it owns.
--
inv lifeline_coverage:
	let uncovered = fragment.covered->asSet()->excludingAll(self.covered)->sortedBy(name) in
	Tuple {
		status = uncovered->isEmpty(),
		message = if uncovered->size() = 1 then
				'Lifeline \'' + uncovered.name->first() + '\' not covered that is covered by owned fragments.'
			else
				'Lifelines ' + asString(quote(uncovered.name)) + ' not covered that are covered by owned fragments.'
			endif
	}

endpackage

Back to the top