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

\chapter{Code Samples (2)}

\section{OCL}

\begin{oclcode}
library mine
	metamodel uml
	require ocl_library_imports
	
	public definitions
	context Edge
	  inv: self.from <> self.to
	  inv: self.oclIsTypeOf(from)
	  inv: self->includes(from)
	  inv: self.allInstances
	  inv: self.isUnique(self)
	  inv: from or to.name = "hello"
	  inv: from and to
	  inv: self->isEmpty()
	  inv: self->exists(from | a)
	  inv: self->forAll(from | a)
	  inv: self.size() = 1
	enddefinitions
endlibrary
\end{oclcode}

\section{Crocopat}

\begin{crocopatcode}
RedirectsTo(a, b) :=
  Page(a) & a != "null" &
  EX(e, EventTrigger(e) &
  eventTriggers(a, e) &
  name(e, "access") &
  Page(b) & b != "null" &
  EX(w, NavigateWire(w) & from(w, e) & to(w, b)));

RedirectsTo(a, b) :=
  Page(a) & Page(b) & TC(RedirectsTo(a, b));

InfiniteRedirect(p) := 
  Page(p) & p != "null" &
  RedirectsTo(p, p);
  
PRINT ["Infinite redirection"] InfiniteRedirect(p);
\end{crocopatcode}

\section{LTL}

\begin{ltlcode}
-- checks for infinite loops

LTLSPEC
  G (operation_running = 1 -> F operation_finished = 1) 
  
LTLSPEC
  -- uses same format as loop.smv
  G ((!(navigation_running = 1 -> !(F navigation_finished = 1))) U navigation_running = 0)
\end{ltlcode}