This repository has been archived by the owner on Apr 13, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathtest.html
130 lines (105 loc) · 5.21 KB
/
test.html
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="fr" xml:lang="fr">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Test for monitors</title>
<link rel="stylesheet" type="text/css" href="style.css" />
<link href="css/ui-lightness/jquery-ui-1.10.1.custom.css" rel="stylesheet">
<script src="js/jquery-1.9.1.js"></script>
<script src="js/jquery-ui-1.10.1.custom.js"></script>
<script type="text/javascript" src="monitor.js"></script>
<script type="text/javascript" src="gui.js"></script>
</head>
<body>
<div id="monitor">
<div>
<p>Input the LTL formula in the box: [<a id="btn-help" href="#">help</a>]</p>
<textarea id="input-formula"></textarea><br />
<p>Or use the following presets:</p>
<select name="preset">
<option value="G ($('#yellowbox').width() < 90)">#yellowbox is always narrower than 90px</option>
<option value="($('#main-title').text() != "Welcome") U ($('#main-title').text() != "Login")">No title Welcome before title Login</option>
<option value="G ($('#yellowbox').position().left == $('#main-title').position().left)">Yellow box always aligned with title</option>
<option value="∀ x ∈ $('#playground li')/.width() : x == 100">All li are 100px wide</option>
<option value="∀ x ∈ $('#yellowbox')/.position().left : G ($('#yellowbox').position().left == x)">The yellow box never moves</option>
<option value="F (∃x ∈ $("li")/.text() : (X ($("#main-title").text() == "x")))">One bullet becomes title in next page</option>
<option value="G (∀ t₁ ∈ $('#playground li')/.text() : X (∃ t₂ ∈ $('#playground li')/.text() : "t₁" == "t₂"))">At least one bullet presists between two pages</option>
</select>
<ul>
<li><input type="button" value="Instantiate a monitor with the formula" id="btn-instantiate" /></li>
<li><input type="button" value="Evaluate monitor on page contents" id="btn-evaluate" /></li>
<!-- <li><input type="button" value="Update monitor's verdict" id="btn-verdict" /></li> -->
</ul>
<p>Current monitor verdict: <span id="verdict-box">no monitor</span></p>
</div>
</div>
<div id="topmenu">
<div>
<h1>LTL Monitor Tester</h1>
<p>A simple page to test various <em>temporal</em> properties
on page attributes.</p>
</div>
</div>
<div id="playground">
<div id="main-title-div">#main-title <h1 id="main-title" title="Double-click to edit">The main title</h1></div>
<div id="yellowbox">#yellowbox</div>
<div id="thelist">#thelist
<ul>
<li style="width:200px" title="Double-click; this element is editable">Item 1</li>
<li style="width:100px" title="Double-click; this element is editable">Item 2</li>
</ul>
</div>
</div>
<div id="help" title="Help on LTL">
<div class="scrollable-contents">
<p>LTL stands for <em>Linear Temporal Logic</em>; it is a formal notation
for expressing constraints along a sequence of states. In the present case,
a state is created each time the monitor processes a new page.</p>
<p>Basic statements can be any JavaScript/jQuery expression that returns a
Boolean. For example:</p>
<code>
$("#menu").height() == 200
</code>
<p>These statements can be combined using the traditional connectives
∧ (and), ∨ (or), → (implies) and ¬ (not). Temporal operators
indicate how these conditions can be sequenced:</p>
<ul>
<li><b>G</b> means "globally". Writing <b>G</b> φ indicates that
φ must evaluate to true in every page</li>
<li><b>F</b> means "eventually". Writing <b>F</b> φ indicates that
φ must evaluate to true in at least one page along the sequence</li>
<li><b>X</b> means "next". Writing <b>X</b> φ indicates that
φ must evaluate to true in the page after the current one</li>
<li><b>U</b> means "until". Writing φ <b>U</b> ψ indicates that
φ must evaluate to true in every page until φ evaluates to true on
some page</li>
</ul>
<p>Hence the following expression indicates that a page with a div called
menu is always followed by a page with a div called user:</p>
<code>
<b>G</b> (($("#menu") != undefined) → (<b>X</b> ($("#user") != undefined)))
</code>
<p>Finally, <em>quantifiers</em> can be used to fetch a set of values from
a page. An expression like ∀<i>x</i> ∈ π : φ
indicates that:</p>
<ul>
<li>The range of values for variable <i>x</i> is obtained by evaluating
π on the current page; π can be any JavaScript expression that
returns an array of strings or integers</li>
<li>When replacing <i>x</i> in φ by any value from the array,
the resulting expression evaluates to true</li>
</ul>
<p>For example, the following expression indicates that at some point,
the text in one of the bullets of a page will become the main heading of the
next page:</p>
<code>
<b>F</b> (∃<i>x</i> ∈ $("li")/.text() : (<b>X</b> ($("#main-title").text() == '<i>x</i>')))
</code>
<p>The monitor allows <tt>/.</tt> as a shorthand notation to fetch values from multiple
elements. For example, to get the height of all elements in class <tt>abc</tt>,
it suffices to write <tt>$(".abc")/.height()</tt>.</p>
</div>
</div>
</body>
</html>