License

NTI is a free software distributed under the terms of the GNU Lesser General Public License, version 3 or any later version. It is developed and maintained by Étienne Payet.

Building nti.jar

Maven is the build tool used to compile the sources, run the tests, and produce the executable jar. The file nti.jar is not built manually: it is generated by Maven.

Prerequisites

You need:

• Java 21 or later
• Maven, or the provided Maven wrapper ./mvnw

Build the jar

From the root of the repository, run:

./mvnw clean package -DskipTests

This builds target/nti.jar without running the test suite.

If you prefer to use a system-wide Maven installation, run:

mvn clean package -DskipTests

After a successful build, the generated jar is located at:

target/nti.jar

You can then run NTI as indicated below.

Using nti.jar

Usage: java -jar target/nti.jar <file> [action] [options]

NTI tries to prove (non)termination of the program in the provided file.

• For logic programs, the implemented techniques are described in [Payet & Mesnard, TOPLAS'06] and [Payet, ICLP'25].
• For TRSs, the implemented technique uses the dependency pair (DP) framework: first, it decomposes the initial set of DP problems into subproblems using sound DP processors, then it tries to prove that the unsolved subproblems are infinite using the approaches of [Payet, TCS'08], [Payet, LOPSTR'18] and [Payet, JAR'24].

file has to conform to the TPDB syntax specification (see here and here). It has one of the following suffixes:

• .pl for a pure logic program
• .ari for a TRS or an SRS in the ARI format
• .xml for a TRS or an SRS in the old XML format
• .trs for a TRS in the old, human-readable, format
• .srs for an SRS in the old, human-readable, format

action (optional) can be:

• -h|--help: print this help
• --version: print the version of NTI
• -print: print the program in the given file
• -stat: print some statistics about the program in the given file
• -patunf=n: apply the pattern unfolding operator n times to the program in the given file and print the result
• -prove: run a (non)termination proof of the program in the given file (THIS IS THE DEFAULT ACTION)

options (optional) can be:

• -v: verbose mode (for printing proof details in the final output)
• -t=n: set a time bound on the nontermination proofs (n is the time bound in seconds)
• -cTI=path: set the path to cTI (for proving termination of logic programs)
  If no path to cTI is set, then only nontermination proofs are run for logic programs