-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathTPCTL.html
136 lines (126 loc) · 7.95 KB
/
TPCTL.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
131
132
133
134
135
136
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"><!-- #BeginTemplate "/Templates/ddd.dwt" --><!-- DW6 -->
<head>
<title>libDDD web site</title><meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" type="text/css" charset="utf-8" media="all" href="files/common.css">
<!--Fireworks MX 2004 Dreamweaver MXarget. Created Sat Oct 14 13:49:59 GMT+0200 ( ) 2006-->
</head>
<body>
<table border="0" cellpadding="0" cellspacing="0" width="900">
<!-- fwtable fwsrc="Haut-metascribe.png" fwbase="Ms-header.gif" fwstyle="Dreamweaver" fwdocid = "1024577916" fwnested="0" -->
<tr>
<td><img src="../images/spacer.gif" width="137" height="1" border="0" alt="" /></td>
<td><img src="../images/spacer.gif" width="567" height="1" border="0" alt="" /></td>
<td><img src="../images/spacer.gif" width="196" height="1" border="0" alt="" /></td>
<td><img src="../images/spacer.gif" width="1" height="1" border="0" alt="" /></td>
</tr>
<tr>
<td rowspan="3"><img name="Hautgauche" src="../images/Haut-gauche.jpg" width="137" height="151" border="0" id="Hautgauche" usemap="#m_HautgaucheMap" alt="" /></td>
<td><img name="Hautcentre" src="../images/Haut-centre.jpg" width="567" height="40" border="0" id="Hautcentre" usemap="#m_HautcentreMap" alt="" /></td>
<td rowspan="2"><img name="Hautdroit" src="../images/Haut-droit-move2.jpg" width="196" height="60" border="0" id="Hautdroit" usemap="#m_HautdroitMap" alt="" /></td>
<td><img src="../images/spacer.gif" width="1" height="40" border="0" alt="" /></td>
</tr>
<tr>
<td><img name="Haut2ms" src="../images/Haut2-ms.jpg" width="567" height="20" border="0" id="Haut2ms" alt="" /></td>
<td><img src="../images/spacer.gif" width="1" height="20" border="0" alt="" /></td>
</tr>
<tr>
<td colspan="2"><img name="Hautbasmeta" src="../images/Haut-bas-ddd.jpg" width="763" height="91" border="0" id="Hautbasmeta" usemap="#m_Hautbasmeta" alt="" /></td>
<td><img src="../images/spacer.gif" width="1" height="91" border="0" alt="" /></td>
</tr>
</table>
<map name="m_HautgaucheMap" id="m_Hautgauche2">
<area shape="rect" coords="0,0,137,151" href="http://www.lip6.fr/en/production/logiciels.php" title="LIP6" alt="LIP6" />
</map>
<map name="m_HautcentreMap" id="m_Hautcentre2">
<area shape="rect" coords="0,0,567,40" href="http://www.lip6.fr" alt="" />
</map>
<map name="m_HautdroitMap" id="m_Hautdroit2">
<area shape="poly" coords="83,0,186,0,186,60,83,60,83,0" href="http://www.upmc.fr" title="UPMC" alt="UPMC" />
<area shape="poly" coords="0,0,83,0,83,60,0,60,0,0" href="http://www.cnrs.fr" title="CNRS" alt="CNRS" />
</map>
<map name="m_Hautbasmeta" id="m_Hautbasmeta">
<area shape="rect" coords="0,62,293,83" href="http://www.lip6.fr/en/recherche/team.php?id=720" title="Move-team" alt="Move-team" />
</map>
<map name="m_Hautgauche" id="m_Hautgauche">
<area shape="rect" coords="0,0,137,151" href="http://www.lip6.fr/en/production/logiciels.php" title="LIP6" alt="LIP6" />
</map>
<map name="m_Hautcentre" id="m_Hautcentre">
<area shape="rect" coords="0,0,567,40" href="http://www.lip6.fr" alt="" />
</map>
<map name="m_Hautdroit" id="m_Hautdroit">
<area shape="poly" coords="83,0,186,0,186,60,83,60,83,0" href="http://www.upmc.fr" title="UPMC" alt="UPMC" />
<area shape="poly" coords="0,0,83,0,83,60,0,60,0,0" href="http://www.cnrs.fr" title="CNRS" alt="CNRS" />
</map>
<map name="m_Hautbasmars" id="m_Hautbasmars">
<area shape="rect" coords="0,62,293,83" href="http://www.lip6.fr/en/recherche/team.php?id=720" title="Move-team" alt="Move-team" />
<area shape="rect" coords="449,7,554,51" href="http://www.lip6.fr/macao" title="Macao" alt="Macao" />
<area shape="rect" coords="276,7,381,51" href="http://www.lip6.fr/framekit" title="FrameKit" alt="FrameKit" />
<area shape="rect" coords="104,6,208,51" href="http://www.lip6.fr/cpn-ami" title="CPN-AMI" alt="CPN-AMI" />
</map>
<table width="900" border="0" cellspacing="0" cellpadding="0">
<tr>
<td width="126" bgcolor="#667F9E" valign="top"> <a title="Macao" href="index.html"><img src="../images/gauche-ddd.jpg" alt="" width="126" height="58" border="0"/></a>
<div class="sidetitle">
<div class="sidetitle"><a class="sidetitle" href="ltl_bench.html">[CAV SUBMISSION]</a></div>
<div class="sidetitle"><a class="sidetitle" href="index.html">About</a></div>
<div class="sidetitle"><a class="sidetitle" href="manual.html">Documents</a></div>
<div class="sidetitle"><a class="sidetitle" href="download.html">Download</a></div>
<div class="sidetitle"><a class="sidetitle" href="bug_report.html">Bug Report</a></div>
<div class="sidetitle"><a class="sidetitle" href="history.html">History</a></div>
</div>
<div class="modDate">
<!-- #BeginDate format:IS1 -->$Date:: 2009-11-12 $<!-- #EndDate -->
</div>
</td>
<td valign="top" bgcolor="#FFFFFF"><table width="774" border="0" cellspacing="0" cellpadding="10">
<tr>
<td bgcolor="#BCC9D6"><a href="http://www.lip6.fr">LIP6</a> > <a href="http://www.lip6.fr/en/production/logiciels.php">Software</a>
> <a href="../index.html">MoVe Sofware</a> > <a href="index.html">SDD/DDD</a>
> <!-- #BeginEditable "chemin" -->Cours CTL M2<!-- #EndEditable --> </td>
</tr>
<tr>
<td bgcolor="#FFFFFF"><!-- #BeginEditable "zoneContenu" -->
Hanoi example <a href="files/hanoi.cpp"> is here</a>.
<h2>Implementation of a CTL model checker.</h2>
<p>This page is meant as a course/tutorial on symbolic CTL model-checking.</p>
<p>Apply the following steps :</p>
<ol>
<li> Download and compile libddd, libits and the ctl packages with <a href="libddd.php#sec:d3svn">this script</a> and <a href="itstools.php#sec:libitsdl">this script</a> </li>
<li> Edit the top of the script to have $SDD point somewhere "reasonable" on your account. </li>
<li> Execute the scripts </li>
<li> Replace the file : ctl/src/mc/ctlCheck.cpp with this one <a href="files/ctlCheck.cpp">this version</a>: edit everywhere marked with TODO. The algorithms to implement are given in <a href="files/M2-GRAR-CTL.pdf">these slides</a></li>
<li> Run the control to make sure your solution is correct : in folder ctl/tests/ run the script run_all.sh. Or run "run_test.pl test_XX.data". Any "test failed" message indicates a problem. Use this set of test data, simply rm *.data and use the files in <a href="files/tests.tgz">this archive</a> instead.</li>
</ol>
<p>
NB : all tests are configured to be run with option "--backward" since you are not asked to implement the forward operators.
</p>
<p> Notations of libddd, where A, B and C are SDD (State in the CTL tool) </p>
<ul>
<li> C = A + B : union of A and B </li>
<li> C = A - B : set difference of A and B </li>
<li> C = A * B : intersection of A and B </li>
<li> State::null : the empty set </li>
<li> getReachable() : a function returning the set of all reachable states.</li>
</ul>
<p> T,U and V are transition relations (Transition::): </p>
<ul>
<li> getNextRel() : returns the transition relation of the system. </li>
<li> getPredRel() : returns predescessor transition relation of the system (backward fire). </li>
<li> C = T(A) : apply T to A, returns successors by a step of T </li>
<li> Transition::id : the identity homomorphism </li>
<li> V = T + U : a transition that returns the sum, for all A, V(A) = T(A) + U(A)</li>
<li> V = T * U : a transition that returns the intersection, for all A, V(A) = T(A) * U(A)</li>
<li> V = T & U : a transition that returns the composition, for all A, V(A) = T( U(A) )</li>
<li> U = fixpoint(T) : build a homomorphism that applies T to fixpoint. </li>
</ul>
<!-- #EndEditable --></td>
</tr>
</table></td>
</tr>
</table>
<img src="../images/Bas.jpg" alt="Bas"/>
</body>
<!-- #EndTemplate --></html>