Tutorial

MVSM 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 MVSM 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, "atime" ranges of the number range 0..9, and "amount" ranges over the number range 0..10, we write

To declare "amt" as a function from "time" to the sort "amount", 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 of sort "amount", we write

MVSM 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 MVSM

Typical invocation of the toolchain script will be mvsm [FILENAME] [CONSTANTS] [NUMBER OF SOLUTIONS] where [FILENAME] is the name of the input file, [CONSTANTS] are of the form "-c [CONST]=[VALUE]". If the number of solutions is omitted, the default value 1 is used. To show all solutions, specify 0 for [NUMBER OF SOLUTIONS]. For example, to obtain one stable model of the leaking bucket example, we write