PLoP - User Manual

If you're too impatient to read this entire document, please check out the examples. But please read this thoroughly at least before submitting any bug reports.

PLoP is basically a tool for evaluating truth values of formulas in given structures. In addition to that, it also can check whether an input file conforms to a specific assignment.

This is the tool that is used for checking your submissions. And you can and should use it also by yourself to be sure that your answers are valid and correct before you submit them. This way, you get immediate feedback e.g. in case there are some syntax errors in your answer.

The tool is supposed to be run from a command line. It needs - as a bare minimum - one command line argument; the file about to be evaluated. It takes other command line arguments as well, but there's more information about that later on.

Please read the examples simultaneously while glancing at the specifications. The input file syntax is meant to be intuitive and easy to digest. You most likely don't want to read the document thoroughly - the examples should give you enough insight to be able to solve the assignments. If you have problems, then review the specification more carefully.


Index

  1. Examples
  2. The PLoP input file structure
  3. About assignment files in general
  4. Invoking the PLoP
  5. Bug reports
  6. Frequently asked questions
  7. Appendix A: Keywords
  8. Appendix B: Command line parameters

Examples

Example 1 - input file in general

The following example is a stand-alone input file - you can evaluate it by invoking the PLoP giving this file's name as the only argument.

(* Example 1: Input file. *)

  % These are single-line comments.

  (* These are multi-line comments. You can ignore them both; that's
     what PLoP does anyway. :) *)

  (* Plop files start first with FORMULAS-section. In this section,
     you define the formulas. *)

true all x. P(x).
false ex x. ~P(x).

  (* After the formulas, the STRUCTURE-section begins. And the
     universe definition must start this section. *)

universe = {a,b,c}.

  (* And then the definitions of predicates, functions and constants -
     in any order you like. *)

predicate P = {a,b}.

As an example of evaluating the input above in any of HUT CC's Unix-machines, follow these steps:

  1. Get yourself a shell prompt. E.g. launch an xterm on any CC's Linux-machine or login via ssh to vipunen.hut.fi.
  2. Start an editor that can write files in 7-bit ASCII format. For example, emacs, vi and pico are good choices. Just launch your favorite editor. Type the above example into the editor, and save the example to a file, e.g. with the name "example1.txt".
  3. Then, back in the shell, invoke PLoP by typing use otter and after that plop example1.txt (assuming that you gave the file the name "example1.txt").

As a result of running PLoP with the example file, you should see output similar to this:

Formula #1 Intended: true. Evaluated to: false --> FAILED
Formula #2 Intended: false. Evaluated to: true --> FAILED

If you have some questions this example didn't answer, you can find the detailed specification of the input file format here.

Example 2 - formulas

The formulas must be entered at the top of the input file. Next, let's see how you should write formula definitions. For reference, check out the connective table.

(* Example 2: formulas-section. *)

  (* Every input file that is to be evaluated should start with at
     least one formula definition. The definition starts with
     the keyword "true" (if the formula *should* evaluate to true) or
     the keyword "false" (if the formula *should* evaluate to
     false). These keywords are case insensitive; you could write them
     like e.g. "TrUe" or "falSE" or with any mixed case, if you think
     that it'd be aesthetically more pleasing. :)

     It is your job then to make them to evaluate to the specified
     truth value - if the formula evaluates to something else, the
     checker reports that the formula evaluation failed. Of course, if
     you're just evaluating some formulas without the assignment - as
     we do here right now - you can ignore the outcome.

     After the keyword comes the formula itself. And the formula is
     terminated with a dot. (Note that quantifiers are also terminated
     with dot!) *)

% Let's write first a formula with some predicates that have no
% arguments:
true P1 & Q1 -> (R1 | P1).

% Next, one with predicates that have lots of arguments, so we get to
% play with the quantifiers too:
false all x. ((ex y. (P2(x,y) & Q2(x,y))) &
              ex y. ex z. ex s. ex t. P5(x,y,z,s,t)).

% Define next the structure in which the formulas will be evaluated.

universe = {one, two, three, four}.

predicate Q1 = {}.
predicate P1 = {<>}.
predicate R1 = {}.

predicate P5 = {<one, two, four, two, one>}.
predicate P2 = {<one, three>, <two, three>}.
predicate Q2 = {<three, three>, <two, two>, <one, one>}.

This example consists of a single file too, so you can evaluate it just like you evaluated the example 1.

As you evaluate this example, the output should be similar to this:

Formula #1 Intended: true. Evaluated to: true --> PASSED
Formula #2 Intended: false. Evaluated to: false --> PASSED

Read the chapter about formulas-section for more information.

Example 3 - predicates and constants

Next, let's check how the predicate and constant definitions work.

(* Example 3 - predicates and constants *)

% First, some example formulas.
true all x. (P(x,a) -> (Q(x) & R(a) & T(a)) | S).

universe = {a,b,c,d,e}.

  (* Next we will define the predicates and constants.

     Any variable that isn't bound can be considered a
     constant. Hence, the "a" in the formula is a constant. Constant
     definition is easy. Write first the "CONSTANT"-keyword, then the
     name of the constant, equation mark, and then the bound
     variable.

     Note that even though "a" is an element in the universe, you must
     still define the constant - otherwise the formula won't be
     evaluated! *)

constant a = c.

  (* Now, let's define the predicates.

     Predicates with no arguments can be either true or false. "{}"
     means false, and "{<>}" means true. *)

predicate S = {}.

  (* Predicates with one or more arguments are defined by stating all
     argument permutations for which the predicate evaluates to
     true. As an example, here we want the predicate R to evaluate to
     true if and only if given the element "c" as argument: *)

predicate R = {c}.

  (* When listing the permutations of a predicate with one argument,
     you can write it in two ways: *)

predicate Q = {a,b,d,e}.
predicate T = {<c>, <e>, <b>}.

  (* But a definition of predicate with two or more arguments must be
     written in the latter style! *)

predicate P = {<a,c>, <b,d>, <e,a>, <e,e>}.

  (* The predicates could also be defined as set equations - for
     example, let's define the predicate R: *)

%predicate R = T difference Q. % Commented out for now.

This is a single file example, so evaluate it like the example 1. As you evaluate this example, the output should be similar to this:

Formula #1 Intended: true. Evaluated to: true --> PASSED

Read the chapters about predicates and constants for more information.

Example 4 - functions

Now it's time to glimpse the functions. Function definitions work almost like predicate definitions.

(* Example 4 - functions *)

true all x. (P(F1(x)) & P(F2(F2(x))) & P(F3(x,C))).

universe = {a,b,c,d}.

predicate P = {a,b}.
constant C = c.

  (* Function maps an argument list of elements to one element in the
     universe. These mappings can be defined using two different
     notations for 1-argument functions: *)

function F1 = {a = b, b = c, c = d, d = a}.
function F2 = {<a> = b, <b> = c,
               <c> = d, <d> = a}.

  (* For a function with 2 or more arguments, you must use this
     notation: *)

function F3 = {<a,a> = a, <a,b> = a, <a,c> = a,
               <a,d> = a, <b,a> = b, <b,b> = b,
               <b,c> = b, <b,d> = b, <c,a> = c,
               <c,b> = c, <c,c> = c, <c,d> = c,
               <d,a> = d, <d,b> = d, <d,c> = d,
               <d,d> = a}.

  (* Note also that you MUST define the mapping for every possible
     argument list! (Wildcards make this job a little bit easier - see
     the next example) *)

This is a single file example, so evaluate it like the example 1. As you evaluate this example, the output should be similar to this:

Formula #1 Intended: true. Evaluated to: false --> FAILED

Read the chapter about functions for more information.

Example 5 - wildcards

The wildcards can be used to shorten the definitions considerably. As an example, let's see how the previous example's function could be shortened:

(* Example 5 - wildcards. *)

function F3 = {

    % First, we'll use the *-wildcard, that expands to all elements in
    % the universe.
    <a,*> = a,
    <b,*> = b,
    <c,*> = c,

    % Next, let's use the sequence-wildcard. With this, we can define
    % sequences of elements and individual elements.
    <d,[a-c]> = d,

    % Third kind of wildcard just copies the first specified argument
    % (its use in this context is quite artificial):
    <d,#1> = a
}.

This isn't a complete file, so you can't evaluate it. But you can replace the definition of the function F3 in the example 4 with this one - they should evaluate to same truth value.

Read the chapter about wildcards for more information.

Example 6 - assignment files in general

This example introduces you to assignment files. Before we go into details, let's first briefly discuss how you can solve the assignments easily - the easiest way is to follow this simple scheme:

  1. Make a copy of the assignment file. For example, if the assignment file's name is assign2a, copy it to a file with name solution2a. Then you can compare your answer to the original assignment later on, after you've made your modifications to the solution2a-file.
  2. Try and solve the assignment by modifying the solution2a-file. For testing whether your solution works, evaluate that file just like in example1.
  3. Before you submit your solution, please check that your solution is still compliant to the assignment after your modifications. You can do this by invoking the PLoP with the --assignment -parameter, like so: /p/edu/T-79.3001/bin/plop solution2a --assignment assign2a. If this results in output that tells you all formulas passed the test, you can submit your solution.

The following is an example of an assignment. After that is shown how you can check your answer against the assignment.

(* Example 6: assignment. *)
true all x. P(x).

universe = {a,b,c,d}.

predicate P = ... . % Fill this yourself!

(* Example 6: answer. *)
true all x. P(x).

universe = {a,b,c,d}.

predicate P = {a,b,c,d}.

Let's save these files with names example6.asgn and example6.answ. First, you should try if the answer evaluates to the intended truth value: /p/edu/T-79.3001/bin/plop example6.answ. You should see the following output:

Formula #1 Intended: true. Evaluated to: true --> PASSED

The next step is to evaluate your answer against the assignment, like this: /p/edu/T-79.3001/bin/plop example6.answ --assignment example6.asgn. You should see the same output:

Formula #1 Intended: true. Evaluated to: true --> PASSED

If, however, you had changed your answer so that it wouldn't be consistent with the assignment any more, the last stage would have noticed it. For example, change the answer's formula's quantifier like this:

(* Example 6: answer. *)
true ex x. P(x).

universe = {a,b,c,d}.

predicate P = {a,b,c,d}.

Now, when you try to check your answer against the assignment
(/p/edu/T-79.3001/bin/plop example6.answ --assignment example6.asgn), you get output like this:

---  ERRORS:  ---
Error while comparing to the assignment file: The answer file's
formula #1 isn't compatible with the corresponding assignment
file's formula.

Read the chapter about assignment files in general for more information.

Example 7 - universe, predicates and constants in assignments

In this example we will examine the assignments more closely, and especially the universe definition and the predicate- and constant definitions.

(* Example 7: assignment - universe, predicates and constants. *)
% First we need some example formulas.
true all x. P(x,c).
false ex x. ~R(x).
false all x. Q(x).
false all x. T(x).

  (* Next line tells you to come up with a universe that has exactly
     four elements, and it's first and second elements are a and b.

     Had there not been the [4], you could have made as big universe
     as you would have wanted to. *)

universe = {a,b,...}[4].

  (* Now the assignment wants you to figure out to what element the
     constant c is mapped to. So replace the "???" with one
     element. *)

constant c = ???.

  (* And next the predicates. The first one states that you have to
     define the predicate P using table definition (i.e. P =
     {<tuples>}.) - that's what the {...} means in this context
     (actually, it says that you have to use 0 or more tuples). *)

predicate P = {...}.

  (* But you can define the predicate R any way you wish - as a table
     or a set equation - since the ... is not inside the braces.

     predicate R = ???. - on the other hand - would accept only set
     equation answers. *)

predicate R = ... .

  (* Next, you have to define the predicate Q by using only one
     tuple. *)

predicate Q = {<...>}.

  (* The next line states that you need to define the predicate T with
     at least three tuples. Two of these tuples have to be the
     elements "a" and "b". *)

predicate T = {<a>,<b>,<...>, ...}.

(* Example 7: answer - universe, predicates and constants. *)
true all x. P(x,c).
false ex x. ~R(x).
false all x. Q(x).
false all x. T(x).

  (* Let's add two elements to the universe, "c" and "d". *)

universe = {a,b,c,d}.

  (* Define the constant c to map to "a". *)

constant c = a.

  (* Then we define the predicate P as a table: *)

predicate P = {<*,a>}.

  (* Note that you can change the order of the predicates compared to
     the assignment. For now, we first want to define the predicate
     Q. We use here only one tuple as the assignment requires. *)

predicate Q = {<d>}.

  (* Next, let's define T like this (three tuples, which was the
     minimum). *)

predicate T = {c,a,b}.

  (* And now we can use the predicates Q and T to define the predicate
     R. *)

predicate R = Q union T.

Try to check your answer now against the assignment, as instructed in example 6. PLoP should print out something like this:

Formula #1 Intended: true. Evaluated to: true --> PASSED
Formula #2 Intended: false. Evaluated to: false --> PASSED
Formula #3 Intended: false. Evaluated to: false --> PASSED
Formula #4 Intended: false. Evaluated to: false --> PASSED

Read the chapters about assignments and universe, predicates and constants for more information.

Example 8 - formulas in assignments

In some assignments you get a fixed structure, but the formulas aren't completely defined. We will next look at some assignment formula examples.

(* Example 8: assignment - formulas. *)

  (* This kind of structure - the ??? without a following connective -
     means that you have to add at least one quantifier in its
     place. *)

true ??? (P(x) -> Q(x)).

  (* The next means that you have to figure out which variables are
     quantified. *)

true all ???. ex ???. (R(x,y)).

  (* The ??? followed or preceded by connective means that you have to
     write a piece of a formula in its place. This formula can contain
     arbitrary many connectives and predicates etc. *)

true all x. (??? -> P(x)).

  (* So the next one means that you have to write one formula which
     evaluates to true. *)

true ???.

% The structure is now completely fixed.
universe = {a,b,c}.

predicate P = {a,b,c}.
predicate Q = {a,b,c}.
predicate R = {<*,c>}.

(* Example 8: answer - formulas. *)

  (* The first one obviously needs an "all x."-quantifier: *)

true all x. (P(x) -> Q(x)).

  (* In the next formula, we have to figure out which of the variables
     is universally quantified. *)

true all x. ex y. (R(x,y)).

  (* Here we can write for example this kind of formula in place of
     the ???: *)

true all x. (Q(x) -> P(x)).

  (* And the last one is really trivial... *)

true ex x. ex y. R(x,y).

  (* You can even define additional formulas below these, if you
     wish. They won't be evaluated while checking your answer against
     the assignment.

     So, even though the next one causes the evaluator to print
     "FAILED", it doesn't matter while checking against the
     assignment. Hence, this solution would pass. *)

true all x. all y. R(x,y).

% And we haven't touched the structure.
universe = {a,b,c}.

predicate P = {a,b,c}.
predicate Q = {a,b,c}.
predicate R = {<*,c>}.

So when you try and evaluate the example answer above alone, as instructed in example 1, the output will be like this:

Formula #1 Intended: true. Evaluated to: true --> PASSED
Formula #2 Intended: true. Evaluated to: true --> PASSED
Formula #3 Intended: true. Evaluated to: true --> PASSED
Formula #4 Intended: true. Evaluated to: true --> PASSED
Formula #5 Intended: true. Evaluated to: false --> FAILED

But when you compare this example answer against the assignment, as instructed in example 6, the PLoP will print output like this:

Formula #1 Intended: true. Evaluated to: true --> PASSED
Formula #2 Intended: true. Evaluated to: true --> PASSED
Formula #3 Intended: true. Evaluated to: true --> PASSED
Formula #4 Intended: true. Evaluated to: true --> PASSED

And thus you know that your answer will pass the test (at least with this example structure).

Read the chapter about formulas in assignment for more information.

Example 9 - functions in assignments

Functions are almost like predicates, but they contain also the mapping from the argument tuple to the corresponding element in the universe.

(* Example 9: assignment - functions. *)

% We need first some formulas.
true all x. all y. P(F(x,y)).

universe = {a,b,c}.

predicate P = {a}.

  (* The answer now needs one tuple that starts with "a", one already
     defined tuple with unspecified mapping, one arbitrary tuple which
     maps to "a", and you can define more tuples freely (note that the
     mapping needs to be defined for all possible tuples).

     ??? in the mapping means that you need to figure out the mapped
     element. *)

function F = {<a,...> = a, <b,a> = ???, <...> = a, ...}.

(* Example 9: answer - functions. *)

% We need first some formulas.
true all x. all y. P(F(x,y)).

universe = {a,b,c}.

predicate P = {a}.

  (* Given the requirements in the assignment, we can easily complete
     the function F like this: *)

function F = {<*,*> = a}.

Now, if you check the answer against the assignment, as instructed in example 6, the PLoP should say something like:

Formula #1 Intended: true. Evaluated to: true --> PASSED

Read the chapter about functions in assignment for more information.

The PLoP input file structure

All keywords are case insensitive. This includes the connectives, section names etc. etc. The names of the variables, constants, predicates and functions, however, are case sensitive.

The input file essentially consist of two distinct parts.

And the structure consist of two parts.

The parts must be in the following order:

  1. The formulas
  2. The definition of the universe.
  3. Definitions of the predicates, functions and constants. Their relative order is not significant - unless there are set equations used in the definitions of the predicates.

The formulas-section

PLoP eats the same syntax as the Tabedit-program's File/Set Root Node -dialog box. You can read about the syntax from there, under the Entering a sentence-section - just write a normal file with your favorite text editor, and give it to the PLoP as an input file. For those who don't have time to read manuals, below is a brief reference table of the connectives and their syntax in PLoP.

Every formula begins with either a TRUE- or a FALSE -keyword. That tells the evaluator - and more important, to you - what the intended truth value of that formula is. In assignment, you then have to complete the partial definitions in such a way that the formula evaluates to the intended truth value.

After the TRUE or the FALSE-keyword comes the formula itself. It consists of atoms and connectives. Atoms may contain terms. The naming conventions of atoms and terms is described in here.

Since the formulas may contain whitespace (tabulators, newlines, spaces), the formula must be terminated with a dot (.).

Connectives

The connectives. The formula refers to any formula, and variable to any variable.
ConnectiveSyntaxPrecedence
Not~Highest
Universal quantifierALL variable. or (ALL variable)Highest
Existential quantifierEX variable. or (EX variable)Highest
Conjunctionformula & formulaMedium
Disjunctionformula | formulaMedium
Implicationformula -> formula or formula --> formulaLowest
Equivalenceformula <-> formulaLowest

You can use as much of parenthesis as you like to change the precedence and to group the formulas as you see fit. Also, chained implications and equivalences are not allowed, naturally.

An example of a formula: TRUE ALL x. ((P(x)) <-> Q(x) & R(F(C,F(C,C)))). Formulas may contain whitespace, i.e. spaces, tabulators and newlines anywhere between the separate tokens. Hence, they must end with dot.

Equivalence predicate

The equivalence predicate - written in input file as = - is a special type of binary predicate. First of all, it is built-in. You can use it anywhere without ever defining it (in fact, it couldn't even be defined, since all names must begin with a letter ranging from "A" to "Z" or with an underscore "_"). Secondly, it's infix-operator, unlike the other predicates, which are prefix-operators. That means that instead of writing =(term,term), you should write term = term. Feel free to use parenthesis around the equivalence predicate, as it enhances the readability a lot.

About the names of the atoms and terms

All of the names given to functions and terms must consist of nothing but upper- or lowercase alphabets ranging from "A" to "Z" and numbers from "0" to "9" and the underscore "_". A name can not start with a number.

In order to keep the formulas easier to read, the names given to predicates, variables, constants and functions must be distinctive. Although it would be lexicographically all right to have e.g. a predicate with name "P" and a function with the same name "P", the formula could easily end up to be totally unreadable to a human. Hence, this restriction is enforced.

Names given to the atoms and terms are case sensitive. You can therefore define e.g. a predicate "Pred" and a function "pred".

Formulas-section in assignments

In assignment file, there might be partially defined formulas. Your job then is to complete the formulas. These formulas contain the special question token ??? somewhere in them.

The token ??? can be in place of a term (inside a predicate, that is), as a quantifier sequence, as a quantifier's variable, or in place of any atom. In the first case, you can complete the formula by writing any term in place of the question token. In the fourth case, complete the formula by replacing the question token with any formula or with any atom.

For example, if the assignment file has a formula like TRUE ALL x. (P(x) & ???)., you can complete that formula with e.g. TRUE ALL x. (P(x) & P(F(x)) | Q(x)). or with e.g. TRUE ALL x. (P(x) & R).

And if the ??? is inside an atom, you can replace it with any term. E.g. the assignment TRUE ALL x. P(???). could be completed e.g. by TRUE ALL x. P(C). (leaving the quantifier in vain) or e.g. by TRUE ALL x. P(f1(f2(f3(f1(f2(f3(x))))))).

The number of ???-tokens specifies the arity of the predicate as well. Hence, if the assignment has a predicate P(???,???) the valid answer predicate must have two arguments too.

If the ???-token appears in the assignment in such place that it isn't immediately preceded or followed by a connective, but it is followed by something else, then you must write one or more quantifiers in its place. For example, either true all x. (P(x,y)). or true all x. ex y. all z. (P(x,y)). is a syntactically valid answer for true ??? (P(???,???)).

With quantifiers, the token ??? can be in place of the quantified variable: ALL ???.. In this case, just figure out which variable the quantifier quantifies, and write its name in place of the ???.

Universe definition

The universe definition must come right after the formulas. The definition can be described with the following regular expression: UNIVERSE = {element (,element)*}. i.e. the universe can define as many elements as necessary. Elements are separated with comma, thus forming a list. The element list must be written inside a pair of braces. The definition must end with a dot.

The universe should - in theory - be a set, but because of the wildcards, the order of the elements is significant. So whenever you change the order of the elements in the universe, you must pay attention to change your wildcards accordingly, if necessary.

The names of the elements must be strings consisting of numbers from "0" to "9" and upper- or lowercase letters ranging from "A" to "Z" and the underscore "_". Names are case sensitive.

Universe definition in assignments

In assignment file, the universe might be only partially defined. In this case, the last element of the universe is .... This means that you should complete the definition. Don't remove any of the predefined elements or change their order!

Additionally, the assignment file may specifically tell you how many elements it expects. In this case there's a [number] at the end of the definition, before the dot. For example: UNIVERSE = {a,b,c,...}[5].

Complete the assignment by introducing new elements at the end of the list. If the size of the universe is specified, introduce as many elements as necessary to fill up that requirement. For example, the following universe would complete the partial definition: UNIVERSE = {a, b, c, first_user_defined, second_user_defined}.

Constant definition

After the universe definition, there can be arbitrary number of constant, predicate and function definitions. Their relative order matters only if there are some predicates defined as set equations.

Constants are terms with arity (number of arguments) of 0. They are thus mapped one element in the universe. This mapping is defined in the following fashion: CONSTANT name = element.

It is impossible to say whether a term with 0 arguments is a variable or a constant. Hence, all terms in a formula, that aren't defined as constants, are considered to be variables. If a quantifier tries to bind a constant, it is an error. It's also an error, if there are free variables in a formula.

Constant definition in assignments

The assignment file might contain constants whose mappings are left unspecified: CONSTANT name = ???. In this case, simply complete the definition by inserting a suitable element in place of the ???.

For example, an assignment's unspecified constant definition CONSTANT C = ???. can be completed with CONSTANT C = element. - the element must then be listed in the universe, of course.

Predicate definition

The predicates can be defined in two different ways: by a truth table (for which arguments the predicate is true) or by a set equation consisting of other predicates and set operators.

Truth table definitions

The definition of a predicate's truth table is similar to the notation used in the course handouts. The definition consists of the keyword PREDICATE, predicate's name, = and the set of argument elements or element tuples with which the predicate evaluates to true, and the definition ends with dot. A tuple is a list of elements, separated with comma, and enclosed in angle brackets, like this: <a,b,c,...>. These tuples can be of any length.

Because the truth table is a set, the order of the single tuples or elements is insignificant in that set.

The form of the set of elements or element tuples depends on the predicate's arity.

Set equation definitions

Another way to define predicates is by writing a set equation. The set equation consists of other predicates connected by set operators. The set relations are listed in the table below. Note that the difference-operator can't be chained.

Set equation operators. The set_eq in the table refers to any set equation.
OperatorSyntaxPrecedence
ComplementCOMPLEMENT set_eqHighest
Unionset_eq UNION set_eqMedium
Intersectset_eq INTERSECT set_eqMedium
Differenceset_eq DIFFERENCE set_eqLowest

The set equation can be defined as follows: Any predicate is a set equation. Any set equation operator that operates a set equation or a pair of set equations is a set equation.

The set equations can be parenthesized in order to make the equation more readable or to change the precedence of operators.

Please note, that all of the predicates in a set equation must have the same arity, and that a predicate used in the set equation must be defined earlier. The latter restriction prevents infinite recursion in set equations.

Hence, e.g. these examples are valid set equations: PREDICATE P = Q., PREDICATE P = COMPLEMENT Q., PREDICATE P = Q UNION S., PREDICATE P = S DIFFERENCE ((Q) UNION COMPLEMENT S). - assuming that the arity of P is equal to the arity of Q and S, and that the predicates used in the set equations are defined earlier.

Predicates in assignments

Assignments might contain partially defined predicates. If a predicate definition contains a question token ??? or a list completion token ..., then you must complete the definition.

Function definition

Definitions of functions are much like the truth table definitions of predicates. The difference is that after each argument tuple or element, there must be the mapping definition: = element. It means that the function maps to the given element with that argument tuple (or element).

Note also that you have to define all of the mappings - that means, there must be a mapping for every permutation of the argument tuple in the given universe. E.g. if the universe is UNIVERSE = {a,b}., then for 2-argument function you have to define a mapping for all argument tuples <a,a>, <a,b>, <b,a>, <b,b>. As an example: FUNCTION F = {<a,a> = a, <a,b> = b, <b,b> = a, <b,a> = a}. Note that here the order of the argument tuple and mapping element entries is insignificant as well.

There's also another way to define the functions. You can just simply list all of the mappings in an ordered set, so that the first element in that set is the mapping for the first argument tuple in the tuple permutation set. E.g. if the universe is UNIVERSE = {a,b}., then you could define the function FUNCTION F = {a, b, a, a}. - this is the same thing as the example function F defined above. The first permutation tuple would then be <a,a>, the second <a,b>, third <b,a> and so forth.

Examples (assume that the universe is defined like UNIVERSE = {a,b,c}.):

As you can see, creating the function definitions can get tedious with even rather small universes and functions with low arity. Hence, you might want to use wildcards instead of writing all permutations by hand. You can read a more in-depth discussion about wildcards later on, but as an example, let's write the 2-argument function with the help of wildcards: FUNCTION F = {<*, #1> = a, <a, [b-c]> = c, <b, [a,c]> = c, <c, [a-b]> = a}.

Function definition in assignments

The assignment file might define some functions only partially, and you must then complete the definition. The partial definitions contain the list completion token ..., and just like with predicates, this token can be found inside a tuple or inside a set.

As an example, the partial definition FUNCTION F = {<a,...> = b, <a,b,c> = c, ...}. is completed by replacing the partial tuple with one starting with <a, and having 3 elements, and by defining the rest of the mappings (as specified by the ... at the end of the set).

The partial definitions might also contain the question token ??? in place of the target element of any mapping. This kind of partial definition is completed by replacing the question token with some element in the universe. As an example, if the assignment defines a function FUNCTION F = {a = a, b = ???}., you can define a function FUNCTION F = {b = b, a = a}. in the answer.

These two can also occur in the same partial definition, e.g. a definition FUNCTION F = {<a,a> = a, <a,b> = b, <b,a> = a, <b,b> = b}. is a syntactically correct answer for the assignment FUNCTION F = {<a,...> = ???, <a,a> = ???, ...}.

Note that you can use the ordered set definition in the answers to the partially defined functions. The assignment can never have these ordered sets defined only partially, but it doesn't mean that you couldn't use them as an answer.

Abbreviating definitions with wildcards

Wildcards are special tokens that can be used in defining predicates or functions. You can replace any element in the definition with a wildcard - but not the function's mapping's target element though. The wildcards then expand into a set of elements.

There are three kinds of different wildcards that you can use.

Comments in input files

There are two types of comments recognized: to-the-end-of-line comments and multi-line comments. The first type of comment begins with % and the comment then goes on to the next newline character. Multi-line comments begin with (* and end with *). The syntax of these, too, follows the Tabedit's definitions.

Everything inside a comment in the input file is simply ignored. The lexer drops the input and doesn't generate lexical tokens out of anything inside a comment.

About assignment files in general

In this course, you get some assignments that are essentially valid input files - lacking only the complete definitions of some parts. It is your task to complete the assignment files so that a) they can be evaluated, and b) the given formulas evaluate to the specified truth value.

You are not allowed to:

You are allowed to, if you wish, add some extra formulas at the end of the formula list. These extra formulas are then ignored silently by the checker during the evaluation of your answer. But you can use the extra formulas for e.g. dividing a large formula of the assignment into smaller parts and checking what the smaller parts evaluate to.

You can read more about the assignment's formulas, universe, constant, predicate and function definitions from the respective sections.

Matching of an answer to an assignment

The assignment file might contain partial definitions in three different structures:

  1. The formulas:

    In assignment file, there can be one or more formulas. The order of the formulas is significant: the first formula in the assignment must be matched by the first formula in the answer file. The checker tries to match the first assignment formula with the first answer formula, and if it fails, it reports an error. Then it tries to match the second ones to each other, then the third ones etc. When it reaches the end of formulas in the assignment file, the checker ignores the rest of the formulas - if there are any additional formulas left - in the answer file.

    Note that, however, when only evaluating, not checking, all of the formulas are evaluated.

  2. The universe:

    The elements in the universe of an answer file must be in the same order as in the assignment file. If the universe is partially defined, e.g. UNIVERSE = {a,b,c,...}., the universe in the answer file must begin with the same elements, e.g. in this case UNIVERSE = {a,b,c.

  3. Predicates, functions and constants:

    The order in which the predicates, functions and constants are defined in the answer file isn't important. The order can be changed compared to the assignment file, as long as the definitions remain still legal (this applies only to the predicate's set equation definitions). The only thing that matters is that all of the predicates, functions and constants that can be found in the assignment file, are also present in the answer file, and that there are no additional predicates, functions or constants defined in the answer file.

    The order of the tuples (or elements) in the predicate table definition is insignificant. As long as the sets are equal (in mathematical sense) to the assignment's, the answer is valid.

    With functions, the order of the entries in the table definition is also insignificant. The answer can also define a function by the ordered set. As long as the resulting mappings are identical, or fulfill the assignments requirements, the answer is considered to be valid.

Special cases in assignment checking

In some assignments your job is to complete a set of formulas. The checker will in these cases generate new structures and try to evaluate your answer also in these new structures. Some of these structures might also be broken - i.e. in these structures the correct answers will fail. These additional structures are used in the checking process in order to e.g. fail tautological answers. Your solution should be valid in every structure imagnable.

The checker also makes it possible to enforce some restrictions for the formulas. For instance, it might be required that your formulas are written into implicative form. These requirements are generally clearly stated in the assignments.

In some cases, the checker also ignores some of the formulas completely. This usually happens with the "broken" structures.

Invoking the PLoP

The PLoP can be found already installed in any of the HUT Computing Centre's UNIX-machines. If you wish, you can install it to your own computer as well (assuming that J2RE is available for your computer). The first two subsections describe how to get the PLoP running, either at HUT CC or in your own computer. Rest of this section discusses about the different modes of PLoP operation and the command line parameters available to you.

Invoking the PLoP at HUT Computing Centre's UNIX-machines

The HUT Computing Centre's UNIX-machines (connect via SSH to one of the UNIX-machines; some are listed in here, or log in to one of the CC's Linux-machines) have the necessary environment already set-up. This is the easiest way to use the PLoP, as you don't need to install or set-up anything yourself.

Once logged in, you can invoke the PLoP by typing in command /p/edu/T-79.3001/bin/plop. Try it, it should say something like "No input files.". If you first run the command use otter, you don't have to write the full path anymore - plain plop works.

The plop script runs the command java -jar /p/edu/T-79.3001/bin/Plop.jar with the given parameters. You can run the PLoP this way too, if you please. Then you can give also some parameters for the java -command as well. (Though this should not be necessary at all, so don't worry about it. Use the script!)

You should give the PLoP then some parameters. For example, if you want to evaluate a file "./test.txt", then you should type in command /p/edu/T-79.3001/bin/plop ./test.txt.

Later on, the phrase "invoke PLoP" should be understood as to type in the command /p/edu/T-79.3001/bin/plop with the specified parameters (or after calling use otter, plop is enough).

Installing the PLoP to your computer and invoking it

First of all, you need Java 2 Runtime Environment (J2RE) version 1.3.1 or newer to be able to run the PLoP. If you don't have it already installed, you can download it (or some newer version) from this official Java site (follow the "Get it Now"-link). Read the installation instructions carefully, and proceed with the install only if you feel confident enough to install Java. If you aren't able to install Java, then just use the pre-installed one at one of Computing Centre's UNIX-machines.

Please note that PLoP isn't still thoroughly tested! If you run PLoP on your computer, you do so on your own responsibility! The safest option is to run it on one of the Computing Centre's UNIX-computers. And to minimize the possible damages if you decide to run it on your computer, never run PLoP logged in as a system administrator (e.g. root in UNIX), if applicable.

Once you have the Java installed, you should open a console (in UNIX) or a dos-prompt (in Windows) and try to execute java-command java -version. If it works, then you're ready to start PLoP. First, download the Plop.jar-package. Save the Plop.jar-file to somewhere - just make sure you remember the path. Then, you can invoke the PLoP by executing java -jar path_toPlop.jar. Now, you should see some output like "No input files.".

You should give the PLoP then some parameters. For example, if you want to evaluate a file "test.txt", then you should type in command java -jar path_toPlop.jar test.txt.

Later on, the phrase "invoke PLoP" should be understood as to type in the command java -jar path_toPlop.jar with the specified parameters.

Simple evaluating

Once you have written your answer to a file using your preferred text editor, you can then evaluate it. Just invoke PLoP with the text file name as an argument. PLoP then evaluates the file and prints out any warnings and errors and the result of the evaluation. Normal invocation has the parameters of the form [options] answer_file_name.

If you have defined predicates, constants or functions that don't exists in any of the formulas, you can turn off the warnings by invoking PLoP with --nowarnAboutUnusedPredicates, --nowarnAboutUnusedFunctions and --nowarnAboutUnusedConstants -options accordingly. The first parameter is useful only when there's a predicate defined with set equation that needs other predicates - that aren't used in the formulas - in the equation. Otherwise, it is recommended to keep the warnings on. After all, you aren't supposed to add any of your own predicate, function or constant definitions to the answer.

If you use wildcards to specify the function mappings or predicate truth tables, two different wildcards in the same definition might expand to intersecting sets of tuples. In this case, the PLoP prints out a warning. These warnings can also be turned off with option --nowarnAboutDuplicateTruthTableEntries for predicates and with option --nowarnAboutDuplicateMappings for functions.

You can get some brief help about the recognized options by invoking PLoP with --help -option. To check the version of the PLoP, use option --version. With these two options, you don't need to specify an input file.

Checking your answer

You can test your answer's conformance to the assignment by giving the answer file as first parameter and the assignment file as the second parameter, prefixed by the --assignment -option. Thus, the assignment checking invocation's parameters are of the form [options] answer_file_name --assignment assignment_file_name.

PLoP will then print out the errors (if the answer doesn't conform to the assignment file) or the result of the evaluation.

Bug reports

First of all, make sure you are using the latest version of the PLoP. The computing centre's vipunen.hut.fi -machine should always have the latest PLoP installed, so invoke the PLoP there with --version -parameter. If you have older PLoP in use, please try the latest version, which you can download here. If the problem persists, then read on.

Before submitting bug report, please first check if the issue has already been discussed in the faq-section of this manual.

Send the bug reports to the address t79144 at tcs.hut.fi. Please start the subject line with [plop-bug]: appended with the bug description. For meaningful bug reports, you should also describe or include the command line parameters (or the complete invocation) you used, the input file(s) you used, the output you got, the computer you used (if not CC's machine, then the operating system) and the version of java runtime library installed (you can figure it out by executing java -version), or if the error appears with the checker, tell us your student number.

Version history
Version Changelog
1.0.0 Initial version

Frequently asked questions

Q: When I check my solution myself with the plop, it prints PASSED to all formulas, but when I submit it, the checker prints output like this:

Failed (thread stopped)
Test failed!

A: This output means that the evaluation of your solution takes so much time, that the checker process decides to stop the evaluation - your solution wouldn't probably be correct anyway.

The error message should be corrected to something more informative in future (x > 1.0.0) versions.

Q: When I check my solution against the assignment like this plop solution3c --assignment assign3c, I get an error message like this:

---  ERRORS:  ---
Error while comparing to the assignment file: The truth table of the predicate "InitOne2" has been altered.

Error while comparing to the assignment file: The truth table of the predicate "InitZero1" has been altered.

I get this error message even though I haven't modified the structure at all; it is an exact copy from the assignment file!

A: This is a bug in the plop version 1.0.0. If the assignment's structure contains predicates which have been defined with empty sets, the comparsion between assignment and even a correct answer will fail.

If you submit a correct answer, it will be succesfully checked though, and you can pass the assignment. This bug only prevents you from testing the solution by hand. The bug will be fixed in the next future release.

Q: When I try to evaluate my answer with plop, it says something like this:

Error in input!
plop.M
        at plop.ab.<init>(Unknown Source)
        at plop.A.<init>(Unknown Source)
        at plop.Plop.a(Unknown Source)
        at plop.Plop.main(Unknown Source)
Token: .

A: The parser of the plop version 1.0.0 has some problems with formulas that have syntax errors in quantifiers. In this case, your answer most probably contains a line with a quantifier like all .x or something like that.

This is a bug in plop, and will be fixed. You can avoid this problem by fixing the syntax errors in your input.

Q: When I check my solution myself, I get PASSED, but when I submit my solution, the output from the checker says something like this:

---  ERRORS:  ---
Error: Formula #1 doesn't comply with requirements: Formula isn't implicative
(The condition of the implication is not a conjunction of atomic formulas (a negation was also seen).).

A: The checker system might enforce some additional restrictions for the solution. In this case, it requires the formula #1 to be in special implicative form. You can check if your solution passes these additional restrictions by giving the checker e.g. the option --implicative <number>, where number corresponds to the formula that should be restricted. You can add more than one options like this, each for one formula.

Appendix A: Keywords

Keywords and their meanings. All keywords are case-insensitive, unless otherwise stated.
Keyword Description See chapter
% Begin an end-to-the-line comment Comments in input files
(* Begin a comment-section Comments in input files
*) End a comment section Comments in input files
TRUE Begin a formula whose intended truth value is true The formulas-section
FALSE Begin a formula whose intended truth value is false The formulas-section
UNIVERSE Begin the universe definition Universe definition
PREDICATE Begin a predicate definition Predicate definition
FUNCTION Begin a function definition Function definition
CONSTANT Begin a constant definition Constant definition
??? Used in place of a definition in assignment file About assignment files in general
... Used in place of a definition in assignment file About assignment files in general
. End a definition The PLoP input file structure
~ Negation Connectives
& Conjunction Connectives
| Disjunction Connectives
-> Implication Connectives
--> Implication Connectives
<-> Equivalence Connectives
( Left parenthesis The formulas-section
) Right parenthesis The formulas-section
ALL Universal quantifier Connectives
EX Existential quantifier Connectives
* Wildcard Wildcards
# Wildcard - must be followed by a number Wildcards
[ Wildcard - begin a sequence definition Wildcards
] Wildcard - end a sequence definition Wildcards
- Separator in sequence-wildcard definitions Wildcards
= This keyword has many meanings: it can be an equivalence-predicate, and it is also used in definitions The PLoP input file structure
{ Begin a set or a table The PLoP input file structure
} End a set or a table The PLoP input file structure
, Separator, used in e.g. sets, tuples and wildcards The PLoP input file structure
< Begin a tuple The PLoP input file structure
> End a tuple The PLoP input file structure
UNION Union-operator in predicate set equations Set equation definitions
INTERSECT Intersection-operator in predicate set equations Set equation definitions
DIFFERENCE Difference-operator in predicate set equations Set equation definitions
COMPLEMENT Complement-operator in predicate set equations Set equation definitions

Appendix B: Command line parameters

The PLoP command line parameters consist of options and the files to be evaluated: [<option parameters>] <answer> [--assignment <assign>]. The only option the PLoP needs is the answer file - file to be evaluated, except when invoked with the --help or --version -option parameters.

In the following the option parameters are listed. Note that some start with "no", which means that that option is switched off. And in case of conflicting option parameters, the last of these parameters in the command line is dominant.

Option parameters.
Parameter Description
--help Print a help message.
--version Print version information.
--timeout <milliseconds> How many milliseconds the checker is allowed to run for each input file. 0 means infinity (default: 0)
--implicative <formula number> Set the requirement for implicative form on for the specified formula.
-- Escape an option. I.e. the next parameter is a filename.
--checkFunctionMappings Check that function is defined for all inputs (default)
--nocheckFunctionMappings Do not check that function is defined for all inputs
--automaticNameConstants Automatically make constants of unbound variables whose names are equivalent to some element in the universe
--noautomaticNameConstants Do not automatically make constants of unbound variables whose names are equivalent to some element in the universe (default)
--warnAboutUnusedPredicates Print warnings of defined predicates that aren't used in the formulas (default)
--nowarnAboutUnusedPredicates Do not print warnings of defined predicates that aren't used in the formulas
--warnAboutUnusedFunctions Print warnings of defined functions that aren't used in the formulas (default)
--nowarnAboutUnusedFunctions Do not print warnings of defined functions that aren't used in the formulas
--warnAboutUnusedConstants Print warnings of defined constants that aren't used in the formulas (default)
--nowarnAboutUnusedConstants Do not print warnings of defined constants that aren't used in the formulas
--warnAboutDuplicateMappings Print warnings of duplicate function mapping entries (default)
--nowarnAboutDuplicateMappings Do not print warnings of duplicate function mapping entries
--warnAboutDuplicateTruthTableEntries Print warnings of duplicate truth table entries (default)
--nowarnAboutDuplicateTruthTableEntries Do not print warnings of duplicate truth table entries

Last update: $Date: 2004/12/02 17:01:16 $