-
Notifications
You must be signed in to change notification settings - Fork 10
/
LICENSE.txt
144 lines (112 loc) · 6.29 KB
/
LICENSE.txt
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
137
138
139
140
141
142
143
144
DiNo is free software; you can redistribute it and/or modify it
under the terms of the GNU Lesser General Public license as
published by the Free Software Foundation; either of the license, or
(at your option) any later version.
DiNo is currently in BETA, and is distributed in the hope that
it will be useful, but WITHOUT ANY WARRANTY; without even the
implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
PURPOSE. See the GNU Lesser General Public license for more details.
You should have received a copy of the GNU Lesser General Public
license along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA.
DiNo builds on Universal Planner Murphi (UPMurphi).
The DiNo/UPMurphi modelling language and state space exploration
algorithm are derived from the CMurphi model checker, which in turn
is derived from the Murphi model checker by Stanford. The planning
algorithms have been developed at the University of L'Aquila, Italy.
SRPG+ heuristic has been developed at King's College London, UK.
To contact the DiNo development team, email to
<wiktor.piotrowski@kcl.ac.uk>
The following is the original Murphi license:
Copyright (C) 1992 - 1999 by the Board of Trustees of Leland
Stanford Junior University.
license to use, copy, modify, sell and/or distribute this software
and its documentation any purpose is hereby granted without royalty,
subject to the following terms and conditions:
1. The above copyright notice and this permission notice must
appear in all copies of the software and related documentation.
2. The name of Stanford University may not be used in advertising
or publicity pertaining to distribution of the software without the
specific, prior written permission of Stanford.
3. This software may not be called "Murphi" if it has been modified
in any way, without the specific prior written permission of David
L. Dill.
4. THE SOFTWARE IS PROVIDED "AS-IS" AND STANFORD MAKES NO
REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF
EXAMPLE, BUT NOT LIMITATION. STANFORD MAKES NO REPRESENTATIONS OR
WARRANTIES OF MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE
OR THAT THE USE OF THE SOFTWARE WILL NOT INFRINGE ANY PATENTS,
COPYRIGHTS TRADEMARKS OR OTHER RIGHTS. STANFORD SHALL NOT BE LIABLE
FOR ANY LIABILITY OR DAMAGES WITH RESPECT TO ANY CLAIM BY LICENSEE
OR ANY THIRD PARTY ON ACCOUNT OF, OR ARISING FROM THE LICENSE, OR
ANY SUBLICENSE OR USE OF THE SOFTWARE OR ANY SERVICE OR SUPPORT.
LICENSEE shall indemnify, hold harmless and defend STANFORD and its
trustees, officers, employees, students and agents against any and
all claims arising out of the exercise of any rights under this
Agreement, including, without limiting the generality of the
foregoing, against any damages, losses or liabilities whatsoever
with respect to death or injury to person or damage to property
arising from or out of the possession, use, or operation of Software
or licensed Program(s) by LICENSEE or its customers.
Notes:
A. Responsible use:
Murphi is to be used as a DEBUGGING AID, not as a means of
guaranteeing the correctness of a design. We do not guarantee that
all errors can be caught with Murphi. There are many reasons for
this:
1. Specifications and verification conditions do not necessarily
capture the conditions necessary for correct operation in practice.
2. Many properties cannot be stated Murphi, including timing
requirements, performance requirements, "liveness" properties (such
as "x will eventually occur") and many others.
3. Murphi cannot verify "large" systems. Almost always, the sizes
of various objects in the description must be modelled as being much
smaller than they are in reality, in order to make verification
feasible. There is a high probability that design errors will only
be manifested when the objects are large.
4. The description of a design may not be consistent with what is
actually implemented.
5. Murphi may have bugs that cause errors to be overlooked.
In short, Murphi is totally inadequate for guaranteeing that there
are no errors; however, it is sometimes effective for discovering
errors that are difficult to detect by other means.
B. Courtesy
Our motivation in distributing this software freely is to encourage
others to evaluate its effectiveness on a wider range of
applications than we have resources to attempt, and to provide a
foundation for further development of automatic verification
techniques.
We would very much appreciate learning about other's experiences
with the system and suggestions for improvements. Even more, we
would appreciate contributions of two kinds: additional verification
examples that can be added to the distribution, and enhancements to
the verification system. Although we do not promise to distribute
the examples or enhancements, we may do so if feasible.
C. Historical Notes
The first version of the Murphi language and verification system was
originally designed in 1990-1991 by David Dill, Andreas Drexler,
Alan Hu, and Han Yang of the Stanford University Computer Systems
Laboratory. The first version of the program was primarily
implemented by Andreas Drexler.
The Murphi language was extensively modified and extended by David
Dill, Alan Hu, Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang
in 1992. The new version was almost entirely reimplemented by Ralph
Melton during the summer and fall of 1992.
The symmetry and multiset reduction was implemented by Norris Ip,
Ulrich Stern added the hash compaction algorithms.
Financial and other support for the design and implementation of
Murphi has come from many sources, the Defense Advanced Research
Projects Agency (under contract number N00039-91-C-0138), the
National Science Foundation (grant number MIP-8858807), the Powell
Foundation, the Stanford Center for Integrated Systems, the U.S.
Office of Naval Research, and Mitsubishi Electronic Laboratories
America. Equipment was provided by Sun Microsystems, the Digital
Equipment Corporation, and IBM.
These notes are based on information provided to Stanford that has
not been independently verified or checked.
D. Support, comments, feedback
If you need help or have comments or suggestions regarding Murphi,
please send electronic mail to "murphi@verify.stanford.edu". We do
not have the resources to provide commercial-quality support, but we
may be able to help you.