McMini 1.0.0 release

COPYING.md

@@ -1,5 +1,5 @@
 McMini is a program that does model checking on a target MultiThreaded Program.
-Copyright (C) 2022, Maxwell Pirtle, Luka Jovanovic, Gene Cooperman
+Copyright (C) 2022-2024, Maxwell Pirtle, Luka Jovanovic, Gene Cooperman
   (pirtle.m@northeastern.edu, jovanovic.l@northeastern.edu, gene@ccs.neu.edu)
 
 This program is free software: you can redistribute it and/or modify

Makefile.in

@@ -35,7 +35,7 @@ test/program/producer_consumer: test/program/producer_consumer.c
 	cd test/program && make producer_consumer
 
 check: all test/program/producer_consumer
-	./mcmini test/program/producer_consumer --quiet
+	./mcmini -f -m 5 test/program/producer_consumer 2 2 0
 
 # If McMini was already built, first do:  'make clean'
 check-gdb: debug test/program/producer_consumer
@@ -46,7 +46,8 @@ check-gdb: debug test/program/producer_consumer
 	  echo After 15 seconds, GDB will start, but it may not work properly.;\
 	  sleep 15; \
 	fi
-	gdb -x gdbinit --args ./mcmini test/program/producer_consumer --quiet
+	# gdb -x gdbinit --args -f -m 5 --quiet ./mcmini test/program/producer_consumer
+	mcmini-gdb -f -m 5 --quiet test/program/producer_consumer
 
 mcmini: src/launch.c libmcmini.so
 	${CC} -g3 -O0 -Iinclude -o $@ $<

NEWS

@@ -0,0 +1,11 @@
+McMini NEWS -- history of user-visible changes.
+
+McMini is distributed at https://github.com/mcminickpt/mcmini
+Please send "Issues" to the github site.
+Please note also the extensive documentation of McMini at:
+    https://mcmini-doc.readthedocs.io/
+
+Version 1.0.0 release notes (Oct. 8, 2024)
+============================================
+This is the first formal release.  Please see the "mcmini-doc"
+documentation, above, for details.

VERSION

@@ -0,0 +1 @@
+1.0.0

configure

@@ -1,8 +1,8 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.71 for McMini 1.0.
+# Generated by GNU Autoconf 2.71 for McMini 1.0.0.
 #
-# Report bugs to <pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu>.
+# Report bugs to <https://github.com/mcminickpt/mcmini/issues>.
 #
 #
 # Copyright (C) 1992-1996, 1998-2017, 2020-2021 Free Software Foundation,
@@ -267,11 +267,10 @@ then :
     printf "%s\n" "$0: be upgraded to zsh 4.3.4 or later."
   else
     printf "%s\n" "$0: Please tell bug-autoconf@gnu.org and
-$0: pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu
-$0: about your system, including any error possibly output
-$0: before this message. Then install a modern shell, or
-$0: manually run the script under such a shell if you do
-$0: have one."
+$0: https://github.com/mcminickpt/mcmini/issues about your
+$0: system, including any error possibly output before this
+$0: message. Then install a modern shell, or manually run
+$0: the script under such a shell if you do have one."
   fi
   exit 1
 fi
@@ -611,10 +610,10 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='McMini'
 PACKAGE_TARNAME='mcmini'
-PACKAGE_VERSION='1.0'
-PACKAGE_STRING='McMini 1.0'
-PACKAGE_BUGREPORT='pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu'
-PACKAGE_URL='https://github.com/mcminickpt/mcmini.git'
+PACKAGE_VERSION='1.0.0'
+PACKAGE_STRING='McMini 1.0.0'
+PACKAGE_BUGREPORT='https://github.com/mcminickpt/mcmini/issues'
+PACKAGE_URL='https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/'
 
 ac_unique_file="src/launch.c"
 # Factoring default headers for most tests.
@@ -1279,7 +1278,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures McMini 1.0 to adapt to many kinds of systems.
+\`configure' configures McMini 1.0.0 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1345,7 +1344,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of McMini 1.0:";;
+     short | recursive ) echo "Configuration of McMini 1.0.0:";;
    esac
   cat <<\_ACEOF
 
@@ -1371,8 +1370,8 @@ Some influential environment variables:
 Use these variables to override the choices made by `configure' or to help
 it to find libraries and programs with nonstandard names/locations.
 
-Report bugs to <pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu>.
-McMini home page: <https://github.com/mcminickpt/mcmini.git>.
+Report bugs to <https://github.com/mcminickpt/mcmini/issues>.
+McMini home page: <https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/>.
 _ACEOF
 ac_status=$?
 fi
@@ -1436,7 +1435,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-McMini configure 1.0
+McMini configure 1.0.0
 generated by GNU Autoconf 2.71
 
 Copyright (C) 2021 Free Software Foundation, Inc.
@@ -1888,7 +1887,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by McMini $as_me 1.0, which was
+It was created by McMini $as_me 1.0.0, which was
 generated by GNU Autoconf 2.71.  Invocation command line was
 
   $ $0$ac_configure_args_raw
@@ -2865,6 +2864,9 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu
 
 
 
+
+
+
 ac_config_headers="$ac_config_headers include/config.h"
 
 
@@ -5946,7 +5948,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by McMini $as_me 1.0, which was
+This file was extended by McMini $as_me 1.0.0, which was
 generated by GNU Autoconf 2.71.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6002,16 +6004,16 @@ $config_files
 Configuration headers:
 $config_headers
 
-Report bugs to <pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu>.
-McMini home page: <https://github.com/mcminickpt/mcmini.git>."
+Report bugs to <https://github.com/mcminickpt/mcmini/issues>.
+McMini home page: <https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/>."
 
 _ACEOF
 ac_cs_config=`printf "%s\n" "$ac_configure_args" | sed "$ac_safe_unquote"`
 ac_cs_config_escaped=`printf "%s\n" "$ac_cs_config" | sed "s/^ //; s/'/'\\\\\\\\''/g"`
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config='$ac_cs_config_escaped'
 ac_cs_version="\\
-McMini config.status 1.0
+McMini config.status 1.0.0
 configured by $0, generated by GNU Autoconf 2.71,
   with options \\"\$ac_cs_config\\"
 

configure.ac

@@ -1,8 +1,11 @@
-#                                               -*- Autoconf -*-
-# Process this file with autoconf to produce a configure script.
+AC_INIT([McMini],
+        m4_esyscmd([tr -d '\n' < VERSION]),
+        [https://github.com/mcminickpt/mcmini/issues],
+        [mcmini],
+        [https://github.com/mcminickpt/mcmini ; https://mcmini-doc.readthedocs.io/])
+
 
 AC_PREREQ([2.71])
-AC_INIT([McMini],[1.0],[pirtle.m@northeastern.edu,jovanovic.l@northeastern.edu,gene@ccs.neu.edu],[mcmini],[https://github.com/mcminickpt/mcmini.git])
 AC_CONFIG_SRCDIR([src/launch.c])
 AC_CONFIG_HEADERS([include/config.h])
 

include/config.h.in

@@ -1,10 +1,83 @@
 /* include/config.h.in.  Generated from configure.ac by autoheader.  */
 
+/* Use debugging flags "-Wall -g3 -O0" */
+#undef DEBUG
+
 /* Define to 1 if you have process_vm_readv and process_vm_writev. */
 #undef HAS_PROCESS_VM
 
-/* define if the compiler supports basic C++14 syntax */
-#undef HAVE_CXX11
+/* Define to 1 if you have the `atexit' function. */
+#undef HAVE_ATEXIT
+
+/* Define to 1 if you have the <fcntl.h> header file. */
+#undef HAVE_FCNTL_H
+
+/* Define to 1 if you have the `fork' function. */
+#undef HAVE_FORK
+
+/* Define to 1 if you have the `ftruncate' function. */
+#undef HAVE_FTRUNCATE
+
+/* Define to 1 if you have the `getpagesize' function. */
+#undef HAVE_GETPAGESIZE
+
+/* Define to 1 if you have the <inttypes.h> header file. */
+#undef HAVE_INTTYPES_H
+
+/* Define to 1 if your system has a GNU libc compatible `malloc' function, and
+   to 0 otherwise. */
+#undef HAVE_MALLOC
+
+/* Define to 1 if you have a working `mmap' system call. */
+#undef HAVE_MMAP
+
+/* Define to 1 if you have the `setenv' function. */
+#undef HAVE_SETENV
+
+/* Define to 1 if you have the <stdint.h> header file. */
+#undef HAVE_STDINT_H
+
+/* Define to 1 if you have the <stdio.h> header file. */
+#undef HAVE_STDIO_H
+
+/* Define to 1 if you have the <stdlib.h> header file. */
+#undef HAVE_STDLIB_H
+
+/* Define to 1 if you have the <strings.h> header file. */
+#undef HAVE_STRINGS_H
+
+/* Define to 1 if you have the <string.h> header file. */
+#undef HAVE_STRING_H
+
+/* Define to 1 if you have the `strtoul' function. */
+#undef HAVE_STRTOUL
+
+/* Define to 1 if you have the <sys/param.h> header file. */
+#undef HAVE_SYS_PARAM_H
+
+/* Define to 1 if you have the <sys/stat.h> header file. */
+#undef HAVE_SYS_STAT_H
+
+/* Define to 1 if you have the <sys/types.h> header file. */
+#undef HAVE_SYS_TYPES_H
+
+/* Define to 1 if you have the <unistd.h> header file. */
+#undef HAVE_UNISTD_H
+
+/* Define to 1 if you have the `vfork' function. */
+#undef HAVE_VFORK
+
+/* Define to 1 if you have the <vfork.h> header file. */
+#undef HAVE_VFORK_H
+
+/* Define to 1 if `fork' works. */
+#undef HAVE_WORKING_FORK
+
+/* Define to 1 if `vfork' works. */
+#undef HAVE_WORKING_VFORK
+
+/* Define to 1 if the system has the type `_Bool'. */
+#undef HAVE__BOOL
 
 /* Define to the address where bug reports for this package should be sent. */
 #undef PACKAGE_BUGREPORT
@@ -23,3 +96,53 @@
 
 /* Define to the version of this package. */
 #undef PACKAGE_VERSION
+
+/* Define to 1 if all of the C90 standard headers exist (not just the ones
+   required in a freestanding environment). This macro is provided for
+   backward compatibility; new code need not use it. */
+#undef STDC_HEADERS
+
+/* Define for Solaris 2.5.1 so the uint32_t typedef from <sys/synch.h>,
+   <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
+   #define below would cause a syntax error. */
+#undef _UINT32_T
+
+/* Define for Solaris 2.5.1 so the uint64_t typedef from <sys/synch.h>,
+   <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
+   #define below would cause a syntax error. */
+#undef _UINT64_T
+
+/* Define to rpl_malloc if the replacement function should be used. */
+#undef malloc
+
+/* Define as a signed integer type capable of holding a process identifier. */
+#undef pid_t
+
+/* Define to the equivalent of the C99 'restrict' keyword, or to
+   nothing if this is not supported.  Do not define if restrict is
+   supported only directly.  */
+#undef restrict
+/* Work around a bug in older versions of Sun C++, which did not
+   #define __restrict__ or support _Restrict or __restrict__
+   even though the corresponding Sun C compiler ended up with
+   "#define restrict _Restrict" or "#define restrict __restrict__"
+   in the previous line.  This workaround can be removed once
+   we assume Oracle Developer Studio 12.5 (2016) or later.  */
+#if defined __SUNPRO_CC && !defined __RESTRICT && !defined __restrict__
+# define _Restrict
+# define __restrict__
+#endif
+
+/* Define to `unsigned int' if <sys/types.h> does not define. */
+#undef size_t
+
+/* Define to the type of an unsigned integer type of width exactly 32 bits if
+   such a type exists and the standard includes do not define it. */
+#undef uint32_t
+
+/* Define to the type of an unsigned integer type of width exactly 64 bits if
+   such a type exists and the standard includes do not define it. */
+#undef uint64_t
+
+/* Define as `fork' if `vfork' does not work. */
+#undef vfork