Browse Source
Missing files from last commit.
Missing files from last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1736 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
16 years ago
3 changed files with 322 additions and 0 deletions
-
31cudd/LICENSE
-
154cudd/MODIFICATIONS
-
137cudd/util/restart.c
@ -0,0 +1,31 @@ |
|||
Copyright (c) 1995-2004, Regents of the University of Colorado |
|||
|
|||
All rights reserved. |
|||
|
|||
Redistribution and use in source and binary forms, with or without |
|||
modification, are permitted provided that the following conditions |
|||
are met: |
|||
|
|||
Redistributions of source code must retain the above copyright |
|||
notice, this list of conditions and the following disclaimer. |
|||
|
|||
Redistributions in binary form must reproduce the above copyright |
|||
notice, this list of conditions and the following disclaimer in the |
|||
documentation and/or other materials provided with the distribution. |
|||
|
|||
Neither the name of the University of Colorado nor the names of its |
|||
contributors may be used to endorse or promote products derived from |
|||
this software without specific prior written permission. |
|||
|
|||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
|||
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
|||
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
|||
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
|||
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
|||
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
|||
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
|||
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
|||
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
|||
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
|||
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
|||
POSSIBILITY OF SUCH DAMAGE. |
|||
@ -0,0 +1,154 @@ |
|||
This file describes the modifications that have been made to this version of CUDD. |
|||
It is based on CUDD 2.4.2. Below is a list of the files that have been changed. |
|||
|
|||
* Makefile |
|||
* setup.sh . |
|||
* shutdown.sh . |
|||
* cudd/cuddAddAbs.c |
|||
* cudd/cuddAddApply.c |
|||
* cudd/cuddAddNeg.c |
|||
* cudd/cuddExport.c |
|||
* cudd/cuddSat.c |
|||
* cudd/cuddTable.c |
|||
* cudd/cudd.h |
|||
* cudd/cuddInt.h |
|||
* util/Makefile |
|||
* util/cpu_time.c |
|||
* util/pipefork.c |
|||
|
|||
The following structural changes have also been made: |
|||
|
|||
* ddmp/nanotrav/mnemosyne/obj/sis and various doc directories have been removed |
|||
* lib directory added with symlinks to lib files |
|||
|
|||
|
|||
Details |
|||
------- |
|||
|
|||
[Makefile] |
|||
|
|||
* Disabled building of nanotrav/mnemosyne packages (don't need) |
|||
|
|||
* Default options are for Linux (original makefile is in Makefile.orig) |
|||
|
|||
------------------ |
|||
|
|||
[setup.sh] |
|||
|
|||
* Don't create links for includes we don't use |
|||
* Create links for libs too |
|||
|
|||
------------------ |
|||
|
|||
[shutdown.sh] |
|||
|
|||
* Delete lib directory too |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddAddAbs.c] |
|||
|
|||
* Added 2 more abstraction functions to do min/max, ie: |
|||
Cudd_addMinAbstract() |
|||
Cudd_addMaxAbstract() |
|||
cuddAddMinAbstractRecur() |
|||
cuddAddMaxAbstractRecur() |
|||
|
|||
* Added another abstraction functions to do "first", ie: |
|||
Cudd_addFirstAbstract() |
|||
cuddAddFirstAbstractRecur() |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddAddApply.c] |
|||
|
|||
* Added the following functions to be used with Cudd_addApply() |
|||
Cudd_addEquals() - f op g = 1 if f==g else 0 |
|||
Cudd_addNotEquals() - f op g = 1 if f!=g else 0 |
|||
Cudd_addGreaterThan() - f op g = 1 if f>g else 0 |
|||
Cudd_addGreaterThanEquals() - f op g = 1 if f>=g else 0 |
|||
Cudd_addLessThan() - f op g = 1 if f<g else 0 |
|||
Cudd_addLessThanEquals() - f op g = 1 if f<=g else 0 |
|||
Cudd_addPow() - power |
|||
Cudd_addMod() - modulo |
|||
Cudd_addLogXY() - log x base y |
|||
|
|||
* Added the following functions to be used with Cudd_addMonadicApply() |
|||
Cudd_addFloor() - floor |
|||
Cudd_addCeil() - ceiling |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddAddNeg.c] |
|||
|
|||
* Changed Cudd_addRoundOff (actually cuddAddRoundOffRecur) so that it rounds |
|||
properly to N decimal places rather than always rounding up. |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddExport.c] |
|||
|
|||
* Changed Cudd_DumpDot: |
|||
- dashed lines for else arcs changed to dotted (more readable on big graphs) |
|||
- the constant node 0 and all arcs to it are not printed |
|||
- labels on nodes omitted |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddSat.c] |
|||
|
|||
* Added the function Cudd_EqualSupNormRel() |
|||
It's very similar to Cudd_EqualSupNorm() but checks for relative difference |
|||
i.e. (f-g/f) < e instead of (f-g) < e |
|||
|
|||
------------------ |
|||
|
|||
[cudd/cuddTable.c] |
|||
|
|||
* Changed cuddUniqueConst so that constants differing by very small amounts |
|||
end up in the same hash table |
|||
|
|||
------------------ |
|||
|
|||
[cudd/{cudd.h,cuddInt.h}] |
|||
|
|||
* Added prototypes for: |
|||
Cudd_addMinAbstract() |
|||
Cudd_addMaxAbstract() |
|||
Cudd_addFirstAbstract() |
|||
Cudd_addEquals() |
|||
Cudd_addNotEquals() |
|||
Cudd_addGreaterThan() |
|||
Cudd_addGreaterThanEquals() |
|||
Cudd_addLessThan() |
|||
Cudd_addLessThanEquals() |
|||
Cudd_addPow() |
|||
Cudd_addMod() |
|||
Cudd_addLogXY() |
|||
Cudd_addFloor() |
|||
Cudd_addCeil() |
|||
Cudd_EqualSupNormRel() |
|||
cuddAddMinAbstractRecur() |
|||
cuddAddMaxAbstractRecur() |
|||
cuddAddFirstAbstractRecur() |
|||
|
|||
------------------ |
|||
|
|||
[util/Makefile] |
|||
|
|||
* Disabled -DUNIX flag so that MingW version compiles OK. |
|||
Don't think we need anything that this adds in. |
|||
|
|||
------------------ |
|||
|
|||
[util/cpu_time.c] |
|||
|
|||
* Extended util_cpu_time() function to work under MingW. |
|||
|
|||
------------------ |
|||
|
|||
[util/pipefork.c] |
|||
|
|||
* Added #ifdef around #include of <sys/wait.h> so that MingW version |
|||
can specify that it doesn't have it. |
|||
|
|||
@ -0,0 +1,137 @@ |
|||
#include <stdio.h> |
|||
#include "util.h" |
|||
|
|||
#if (defined(sun) && ! defined(sparc)) || defined(vax) |
|||
|
|||
#include <signal.h> |
|||
#include <sys/types.h> |
|||
#include <sys/time.h> |
|||
|
|||
static char *save_stack_base; |
|||
static char *stack_lo_addr; |
|||
static char *stack_hi_addr; |
|||
static int stack_size; |
|||
|
|||
static int restart_global_flag; |
|||
static char *old_file_name; |
|||
static char *new_file_name; |
|||
|
|||
char *util_save_sp; /* set by util_restart_save_state() */ |
|||
extern char *sbrk(); |
|||
|
|||
static void |
|||
grow_stack() |
|||
{ |
|||
int i, space[256]; |
|||
|
|||
for(i = 0; i < 256; i++) { |
|||
space[i] = 0; |
|||
} |
|||
if ((char *) &i > stack_lo_addr) { |
|||
grow_stack(); |
|||
} |
|||
} |
|||
|
|||
|
|||
/* ARGSUSED */ |
|||
static int |
|||
handle_sigquit(int sig, int code, struct sigcontext *scp) |
|||
{ |
|||
if (util_restart_save_state()) { |
|||
/* we are restarting ! -- return from signal */ |
|||
|
|||
} else { |
|||
/* copy stack to user data space */ |
|||
stack_lo_addr = util_save_sp; |
|||
stack_size = stack_hi_addr - stack_lo_addr + 1; |
|||
save_stack_base = sbrk(stack_size); |
|||
(void) memcpy(save_stack_base, stack_lo_addr, stack_size); |
|||
|
|||
/* write a new executable */ |
|||
(void) fprintf(stderr, "Writing executable %s ...\n", new_file_name); |
|||
(void) util_save_image(old_file_name, new_file_name); |
|||
|
|||
/* terminate if signal was a QUIT */ |
|||
if (sig == SIGQUIT) { |
|||
(void) _exit(1); |
|||
} |
|||
} |
|||
} |
|||
|
|||
|
|||
static void |
|||
restart_program() |
|||
{ |
|||
(void) fprintf(stderr, "Continuing execution ...\n"); |
|||
|
|||
/* create the stack */ |
|||
grow_stack(); |
|||
|
|||
#ifdef vax |
|||
asm("movl _util_save_sp,sp"); |
|||
#endif |
|||
#ifdef sun |
|||
asm("movl _util_save_sp,sp"); |
|||
#endif |
|||
|
|||
/* copy the stack back from user space */ |
|||
(void) memcpy(stack_lo_addr, save_stack_base, stack_size); |
|||
|
|||
/* remove the sbrk for the stack */ |
|||
if (sbrk(-stack_size) < 0) { |
|||
perror("sbrk"); |
|||
} |
|||
|
|||
util_restart_restore_state(); /* jump back into handle_sigquit() */ |
|||
} |
|||
|
|||
void |
|||
util_restart(char const *old, char const *neW, int interval) |
|||
{ |
|||
struct itimerval itimer; |
|||
|
|||
#ifdef vax |
|||
#ifdef ultrix |
|||
stack_hi_addr = (char *) 0x7fffe3ff; /* ultrix */ |
|||
#else |
|||
stack_hi_addr = (char *) 0x7fffebff; /* bsd 4.3 */ |
|||
#endif |
|||
#endif |
|||
#ifdef sun |
|||
stack_hi_addr = (char *) 0x0effffff; /* Sun OS 3.2, 3.4 */ |
|||
#endif |
|||
|
|||
old_file_name = old; |
|||
new_file_name = neW; |
|||
|
|||
(void) signal(SIGQUIT, handle_sigquit); |
|||
|
|||
if (interval > 0) { |
|||
(void) signal(SIGVTALRM, handle_sigquit); |
|||
itimer.it_interval.tv_sec = interval; |
|||
itimer.it_interval.tv_usec = 0; |
|||
itimer.it_value.tv_sec = interval; |
|||
itimer.it_value.tv_usec = 0; |
|||
if (setitimer(ITIMER_VIRTUAL, &itimer, (struct itimerval *) 0) < 0) { |
|||
perror("setitimer"); |
|||
exit(1); |
|||
} |
|||
} |
|||
|
|||
if (restart_global_flag) { |
|||
restart_program(); |
|||
} |
|||
restart_global_flag = 1; |
|||
} |
|||
|
|||
#else |
|||
|
|||
/* ARGSUSED */ |
|||
void |
|||
util_restart(char const *old, char const *neW, int interval) |
|||
{ |
|||
(void) fprintf(stderr, |
|||
"util_restart: not supported on your operating system/hardware\n"); |
|||
} |
|||
|
|||
#endif |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue