TarTar Version 2.7.0

License.txt

@@ -0,0 +1,7 @@
+Copyright (c) 2019
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.  

Readme.txt

@@ -1 +1,13 @@
  We will publish the source code of TarTar with an installation manual soon ...
+
+ TarTar itself is licensed by the MIT license.
+
+ TarTar includes several other tools that are published under other licenses:
+ - LTSmin [https://ltsmin.utwente.nl/]
+ - opaal [http://opaal-modelchecker.com/opaal-ltsmin/]
+ - pyuppaal [https://launchpad.net/pyuppaal]
+ - pydbm [http://people.cs.aau.dk/~adavid/UDBM/]
+
+ - Uppaal [http://www.uppaal.org/] (download necessary)
+ - Z3 [https://github.com/Z3Prover/z3] (download necessary)
+

ltsmin-3.0.2/AUTHORS

@@ -0,0 +1,17 @@
+Stefan Blom <[email protected]>
+Jeroen Ketema <[email protected]>
+Alfons Laarman <[email protected]>
+Elwin Pater <[email protected]>
+Jaco van de Pol <[email protected]>
+Michael Weber <[email protected]>
+Gijs Kant <[email protected]>
+Tom van Dijk <[email protected]>
+Jeroen Meijer <[email protected]>
+
+Contributors:
+Axel Belinfante <[email protected]>
+Simona Orzan <[email protected]>
+Jeroen van der Wulp <[email protected]>
+Jeroen Keiren <[email protected]>
+
+Please send bug reports to <[email protected]>.

ltsmin-3.0.2/CODING-STANDARDS

@@ -0,0 +1,142 @@
+Language
+========
+
+* No C/C++ header file may reference config.h.
+
+* All C/C++ source files must include config.h before any other included file:
+  #include <hre/config.h>
+
+* All other included headers should come in alphabetical order after config.h
+  to enable easy lookup and avoid duplicates. This also applies to file 
+  listings in, for example, Makefile.am.
+
+* Keep #include directives ordered like this:
+    system headers
+    external dependencies
+    ltsmin headers
+
+  Each block should be separated by a blank line.
+
+* Always use #include <...>, never use #include "...".
+
+* Ensure that all C/C++ source code compiles under "-W -Wall -Werror".
+
+  Unused variables will cause warnings, and thus should be flagged
+  explicitly at the end of a function, like this: 
+
+    // ...
+    return;
+    (void)a; (void)b;
+
+* Prefer "static const" over #define whenever possible.  Use enums for
+  logically-connected groups of constants.
+
+* Declare all functions local to a compilation unit as "static".
+
+* Use asserts to document and enforce invariants.  Remember to
+  #include <assert.h>.  Assert expressions must be free of function
+  calls and side effects, e.g.: use "int max = f(); assert (i < max); i++;"
+  instead of "assert (i++ < f());".
+
+* Functions which can fail should return 0 on success, and a non-zero
+  error code to indicate failure.  For functions which return pointers
+  and have only a single failure mode, NULL can be returned to
+  indicate failure.
+
+* Boolean negation (!b) should not be used to test for NULL pointers
+  or (non-)zero error codes.  Instead, use (ptr != NULL) or (ret != 0).
+
+* Use size_t or ssize_t to represent counters.  They can be printf()ed
+  with "%zu" or "%zd" directives.
+
+
+Naming
+======
+
+* For identifiers generally follow the usual C conventions of
+  lower-case letters and underscores, e.g., trc_get_edge_label.
+
+* For identifiers which are part of a submodule, use a (short but
+  mnemonic) unique prefix which distinguishes them from other
+  submodules, e.g., "log_printf" (prefix "log_" for all logging
+  related functions and structs).
+
+* Ensure that exported identifiers do not clash with system or
+  third-party code, e.g., by making them suitably long or using
+  prefixes.
+
+* For global variables use identifiers consisting of three or more
+  letters, with the first letter capitalized.  For global constants,
+  use identifiers in all upper-case.  For macros, use all upper-case,
+  except if they replace a function (in which case they should follow
+  function naming conventions).
+
+* Avoid unnecessary and ambiguous abbreviations of identifiers (like
+  "ex_program" for "exit_program"; a shorter identifier would be
+  "die").  However, idiomatic abbreviations are allowed (e.g., "buf"
+  for "buffer", "xlate" for "translate", etc.).
+
+* For typedefs use names ending with "_t", e.g.,
+  "typedef struct foo foo_t;"
+
+
+Source Organization
+===================
+
+* External subsystems (e.g., libraries, parser generators) should be kept in
+  separate sub-directories below the top-level directory.
+
+* Subsystems should be kept in separate sub-directories below src/.
+
+
+Style
+=====
+
+* No Tab (ASCII 9) maybe be introduced in any source file.  It is
+  advisable to configure the editor to ensure this.
+
+* Indentation is 4 spaces per level.
+
+* Avoid more than 80 characters per line.
+
+* Avoid long functions (> 100 lines of code) and deep nesting.
+  Instead, break up code into smaller logical units; use meaningful
+  names.
+
+* Avoid writing functions with long parameter lists.  Avoid passing
+  more than two logically-connected parameters separately.  Instead
+  consider boxing them into a struct.
+
+* Code layout for new files (or substantial changes to existing code)
+  follows GNU Indent with the following options:
+
+======================== ~/.indent.pro =========================
+-orig -nut -i4 -bs -br -ce -cdw -ncdb -pcs -ncs -cd40 -c40 -di20
+================================================================
+
+  In particular, opening braces should be placed on the same line,
+  with the exception of function definitions.  Note that the function
+  name should be placed on the first column:
+
+static int *
+foo (int x, int y, int z)
+{
+    if (x < 0) {
+        // statements
+    } else if (x > 0) {
+        // statements
+    } else {
+        // statements
+    }
+
+    switch (y) {
+    case 0:
+        // statements
+    default:
+        // statements
+    }
+
+    return NULL;
+}
+
+* To improve code readability, use whitespace between tokens.

ltsmin-3.0.2/COPYING

@@ -0,0 +1,29 @@
+Copyright (c) 2008 - 2018 Formal Methods and Tools, University of Twente
+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 Twente 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.