~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/shumsky/slides2_files/slide0009.htm

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
<html xmlns:v="urn:schemas-microsoft-com:vml"
 
2
xmlns:o="urn:schemas-microsoft-com:office:office"
 
3
xmlns:p="urn:schemas-microsoft-com:office:powerpoint"
 
4
xmlns="http://www.w3.org/TR/REC-html40">
 
5
 
 
6
<head>
 
7
<meta http-equiv=Content-Type content="text/html; charset=windows-1252">
 
8
<meta name=ProgId content=PowerPoint.Slide>
 
9
<meta name=Generator content="Microsoft PowerPoint 9">
 
10
<link id=Main-File rel=Main-File href="../slides2.htm">
 
11
<link rel=Preview href=preview.wmf>
 
12
<!--[if !mso]>
 
13
<style>
 
14
v\:* {behavior:url(#default#VML);}
 
15
o\:* {behavior:url(#default#VML);}
 
16
p\:* {behavior:url(#default#VML);}
 
17
.shape {behavior:url(#default#VML);}
 
18
v\:textbox {display:none;}
 
19
</style>
 
20
<![endif]-->
 
21
<title>Developing a Framework for Simulation, Verification and Testing of SDL
 
22
Specifications</title>
 
23
<meta name=Description content="3-Nov-00: Activator">
 
24
<link rel=Stylesheet href="master03_stylesheet.css">
 
25
<![if !ppt]>
 
26
<style media=print>
 
27
<!--.sld
 
28
        {left:0px !important;
 
29
        width:6.0in !important;
 
30
        height:4.5in !important;
 
31
        font-size:107% !important;}
 
32
-->
 
33
</style>
 
34
<script src=script.js></script><script><!--
 
35
gId="slide0009.htm"
 
36
if( !IsNts() ) Redirect( "PPTSld", gId );
 
37
//-->
 
38
</script><!--[if vml]><script>g_vml = 1;
 
39
</script><![endif]--><script for=window event=onload><!--
 
40
if( !IsSldOrNts() ) return;
 
41
if( MakeNotesVis() ) return;
 
42
LoadSld( gId );
 
43
MakeSldVis(0);
 
44
//-->
 
45
</script><![endif]><o:shapelayout v:ext="edit">
 
46
 <o:idmap v:ext="edit" data="10"/>
 
47
</o:shapelayout>
 
48
</head>
 
49
 
 
50
<body lang=EN-US style='margin:0px;background-color:white'
 
51
onclick="DocumentOnClick()" onresize="_RSW()" onkeypress="_KPH()">
 
52
 
 
53
<div id=SlideObj class=sld style='position:absolute;top:0px;left:0px;
 
54
width:534px;height:400px;font-size:16px;background-color:white;clip:rect(0%, 101%, 101%, 0%);
 
55
visibility:hidden'><p:slide coordsize="720,540"
 
56
 colors="#FFFFFF,#000000,#808080,#000000,#00CC99,#3333CC,#CCCCFF,#B2B2B2"
 
57
 masterhref="master03.xml">
 
58
 <p:shaperange href="master03.xml#_x0000_s1025"/><![if !ppt]><p:shaperange
 
59
  href="master03.xml#_x0000_s1028"/><p:shaperange
 
60
  href="master03.xml#_x0000_s1029"/><![endif]><p:shaperange
 
61
  href="master03.xml#_x0000_m1026"/><v:shape id="_x0000_s10242" type="#_x0000_m1026"
 
62
  style='position:absolute;left:54pt;top:14.5pt;width:612pt;height:60pt'>
 
63
  <v:fill o:detectmouseclick="f"/>
 
64
  <v:stroke o:forcedash="f"/>
 
65
  <o:lock v:ext="edit" text="f"/>
 
66
  <v:textbox style='mso-fit-shape-to-text:t'/>
 
67
  <p:placeholder type="title"/></v:shape><p:shaperange
 
68
  href="master03.xml#_x0000_m1027"/><v:shape id="_x0000_s10243" type="#_x0000_m1027"
 
69
  style='position:absolute;left:27pt;top:89.25pt;width:666pt;height:442pt'>
 
70
  <v:fill o:detectmouseclick="f"/>
 
71
  <v:stroke o:forcedash="f"/>
 
72
  <o:lock v:ext="edit" text="f"/>
 
73
  <v:textbox style='mso-fit-shape-to-text:t'/>
 
74
  <p:placeholder type="body" position="1"/></v:shape>
 
75
 <div v:shape="_x0000_s10242" class=T style='position:absolute;top:3.25%;
 
76
 left:8.42%;width:83.14%;height:10.0%'>Activator</div>
 
77
 <div v:shape="_x0000_s10243" class=B><span style='position:absolute;
 
78
 top:17.25%;left:8.42%;width:102.43%'><span style='font-size:88%'><span
 
79
 style='mso-special-format:bullet;position:absolute;left:-3.65%'>�</span></span><span
 
80
 style='font-size:88%'>SDL differentiates between process definition and </span></span><span
 
81
 style='position:absolute;top:23.5%;left:8.42%;width:86.89%'><span
 
82
 style='font-size:88%'>process instance&#13;</span></span>
 
83
 <div style='position:absolute;top:31.0%;left:4.68%;width:90.63%;height:6.5%'><span
 
84
 style='position:absolute;top:0%;left:4.13%;width:95.86%'><span
 
85
 style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
 
86
 left:-4.31%'>�</span></span><span style='font-size:88%'>Defined process
 
87
 activation mechanism&#13;</span></span></div>
 
88
 <div style='position:absolute;top:38.25%;left:4.68%;width:90.63%;height:6.5%'><span
 
89
 style='position:absolute;top:0%;left:4.13%;width:95.86%'><span
 
90
 style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
 
91
 left:-4.31%'>�</span></span><span style='font-size:88%'>Receiver process
 
92
 instance&#13;</span></span></div>
 
93
 <div style='position:absolute;top:45.5%;left:4.68%;width:90.63%;height:5.75%'><span
 
94
 style='mso-special-format:nobullet;display:none'>�</span><span
 
95
 style='font-size:75%'><span style='mso-tab-count:1;width:4.13%'> </span></span><span
 
96
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b>(1
 
97
 receiverprocess start &#13;</b></span></div>
 
98
 <div style='position:absolute;top:52.0%;left:4.68%;width:90.63%;height:4.5%'><span
 
99
 style='mso-special-format:nobullet;display:none'>�</span><span
 
100
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
 
101
 style='mso-tab-count:1;width:4.13%'> </span><span style="mso-spacerun: yes">�
 
102
 </span>((ackid . nil) (frameid . nil) (self . 1) &#13;</b></span></div>
 
103
 <div style='position:absolute;top:57.5%;left:4.68%;width:100.74%;height:4.5%'><span
 
104
 style='mso-special-format:nobullet;display:none'>�</span><span
 
105
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
 
106
 style="mso-spacerun: yes">� </span><span style='mso-tab-count:1;width:.41%'> </span><span
 
107
 style="mso-spacerun: yes">���</span>(sender . nil) (parent . 0) (offspring .
 
108
 nil) &#13;</b></span></div>
 
109
 <div style='position:absolute;top:62.75%;left:4.68%;width:90.63%;height:4.5%'><span
 
110
 style='mso-special-format:nobullet;display:none'>�</span><span
 
111
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
 
112
 style="mso-spacerun: yes">��� </span>((start �)) nil)&#13;</b></span></div>
 
113
 <span style='position:absolute;top:68.25%;left:8.42%;width:95.5%'><span
 
114
 style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
 
115
 left:-3.92%'>�</span></span><span style='font-size:88%'>Correctness property:
 
116
 defined a recognizer for </span></span><span style='position:absolute;
 
117
 top:74.5%;left:8.42%;width:86.89%'><span style='font-size:88%'>valid instances
 
118
 of a system&#13;</span></span>
 
119
 <div style='position:absolute;top:81.5%;left:4.68%;width:90.63%;height:5.75%'><span
 
120
 style='mso-special-format:nobullet;display:none'>�</span><span
 
121
 style='font-size:75%'><span style='mso-tab-count:1;width:4.13%'> </span></span><span
 
122
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b>(defthm
 
123
 activate-makes-instance&#13;</b></span></div>
 
124
 <div style='position:absolute;top:88.25%;left:4.68%;width:90.63%;height:4.5%'><span
 
125
 style='mso-special-format:nobullet;display:none'>�</span><span
 
126
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
 
127
 style='mso-tab-count:1;width:4.13%'> </span><span style="mso-spacerun: yes">�
 
128
 </span>(implies (wf-type S) &#13;</b></span></div>
 
129
 <div style='position:absolute;top:93.5%;left:4.68%;width:90.63%;height:4.5%'><span
 
130
 style='mso-special-format:nobullet;display:none'>�</span><span
 
131
 style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
 
132
 style="mso-spacerun: yes">������������ </span>(wf-instance (activate S) S)))</b></span></div>
 
133
 </div>
 
134
</p:slide></div>
 
135
 
 
136
</body>
 
137
 
 
138
</html>