Tutorial

ASPMT Declarations

The tutorial describes the leaking bucket example. Consider a leaking bucket with maximum capacity c that loses one unit of water every time step by default. The bucket can be refilled to its maximum capacity by the action fill. The initial capacity is 5 and the desired capacity is 10. Here, the argument variable corresponding to the length of the plan increases so both systems suffer scalability issues.

Declarations in ASPMT are used to specify the valid ranges of values for arguments of functions and for functions themselves. In addition, they allow specification of user-defined sorts. They also specify the sorts of variables (if a variable is not declared it is understood to be a numeric variable). To declare two user defined sorts "atime" and "time", we write

To specify that "time" ranges over the number range 0..10 and "atime" ranges of the number range 0..9, we write

To declare "amt" as a function from "time" to the real interval [0,10], "weight" as a function from "time" to the real interval [0,5], and "fill" as a function from "atime" to boolean values, we write

To declare T as a variable of sort "time", ST as a variable of sort "atime", and X as a variable over the number range 0..10, we write

ASPMT Formulas

The multi-valued propositional rules are formed using the constants, variables, objects, and propositional connectives, which include & (conjunction), | (disjunction), -> (implication), <- (reverse direction implication), not (negation). Below is an annotated example.

Running ASPMT2SMT

Typical invocation of the toolchain script will be aspmt2smt [FILENAME] [CONSTANTS] where [FILENAME] is the name of the input file, [CONSTANTS] are of the form "-c [CONST]=[VALUE]". For example, to run the leaking bucket example, we write