Skip to content

Temporal Equilibrium Logic (TEL)

A Temporal Equilibrium Logic extension of ASP.

Usage

For the encoding in instances/paper-lights.lp you can run the following command to get all traces of length 3:

> metasp solve clingo  -c n=2 instances/paper-lights.lp --syntax-encoding syntax.lp --semantics-encoding semantics.lp  -n 0
Metasp (<class 'metasp.app.ClingoApp'>) version 5.8.0
Reading from instances/paper-lights.lp
Solving...
Answer: 1 (Time: 0.128s)
true(light(l1),0) true(light(l1),1) true(light(l1),2) true(green(l1),2) true(red(l1),0) true(red(l1),1) true(push(l1),1)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.129s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.121s

By adding the --printer temporal_printer argument you can get a more readable output:

> metasp solve clingo  -c n=2 instances/paper-lights.lp --syntax-encoding syntax.lp --semantics-encoding semantics.lp  --printer temporal_printer -n 0
Metasp (<class 'metasp.app.ClingoApp'>) version 5.8.0
Reading from instances/paper-lights.lp
Solving...
Answer: 1 (Time: 0.133s)
 State 0: light(l1) red(l1)
 State 1: light(l1) push(l1) red(l1)
 State 2: green(l1) light(l1)

SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.134s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.118s

Show statements

Notice this only shows the atoms, formulas can be included by adding the corresponding #show directive in the input file.

For instance, adding the following code to the instances/paper-lights.lp file will show the atom green and the formula &next in the output:

#show &next/1.
#show green(L):green(L).
#show.

> metasp solve clingo  -c n=2 instances/paper-lights.lp --syntax-encoding syntax.lp --semantics-encoding semantics.lp  --printer temporal_printer -n 0 --log warning
Metasp (<class 'metasp.app.ClingoApp'>) version 5.8.0
Reading from instances/paper-lights.lp
Solving...
Answer: 1 (Time: 0.124s)
 State 0: &next(&eventually(green(l1))) &next(push(l1))
 State 1: &next(&eventually(green(l1)))
 State 2: green(l1)

SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.125s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.122s

UI

To run the UI use the following command:

metasp ui --meta-config config.yml --log info -c n=3 instances/paper-lights.lp

Example

Traffic Lights

light(l1).
red(L) :- not green(L), light(L).
&next(push(l1)) :- &initial.

&next(&eventually(green(L))):- push(L).

Definition of the system

Configuration

syntax-encoding:
  - "./syntax.lp"
semantics-encoding:
  - "./semantics.lp"
printer: temporal_printer
ui-encoding:
  - "./ui.lp"
required-constants:
  - "n"

Syntax

#type tel {
  expressions: {
    &true/0;
    &not/1: { type: tel, safety: unsafe; };
    &initial/0;
    &next/1: {
      type: tel, safety: safe;
    };
    &prev/1: {
      type: tel, safety: safe;
    };
    &eventually/1: {
      type: tel, safety: safe;
    };
  };
  subtypes: { atom; };
  macros:   { &final: &not(&next(&true)); };
  occurrence: any;
}.

Semantics

Uses the provided standard encodings:

semantics.lp

Encoding

Semantics encoding for Temporal Equilibrium Logic (TEL)

Included standard encodings

#include "metasp.meta-time.lp".
#include "metasp.show-time.lp".
#include "metasp.reify-defined.lp".
#include "metasp.reify-defined-metasp.lp".

Operators

&true
true(&true,K) :- formula(tel,&true), time(K).
&initial
true(&initial,0) :- formula(tel,&initial).
:- formula(tel,&initial), true(&initial,K), K!=0.
&next
true(F,K+1) : time(K+1) :- formula(tel,&next(F)), true(&next(F),K).
true(&next(F),K) :- formula(tel,&next(F)), true(F,K+1), time(K).
&prev
true(F,K-1) : time(K-1) :- formula(tel,&prev(F)), true(&prev(F),K).
true(&prev(F),K) :- formula(tel,&prev(F)), true(F,K-1), time(K).
&eventually
true(F,J) : time(J), K<=J :- true(&eventually(F),K).
true(&eventually(F),K) :- formula(tel,&eventually(F)), true(F,J), K<=J, time(K), time(J).
&not
true(&not(F),K) :- formula(tel,&not(F)), not true(F,K), time(K).
:- true(&not(F),K), true(F,K), time(K).

UI

Extension to UI encoding to label formulas

ui.lp

Encoding

#script (python)
from clingo.symbol import String, Number
def tel_label(formula):
    args = formula.arguments
    name = formula.name
    if name == "__true":
        return "⊤"#For some reason the other top is printing a strange character on the pdf format
    if name == "__false":
        return "⊥"
    if name == "__initial":
        return "I"
    if name == "__final":
        return "F"
    if name == "__next":
        return "○"+tel_label(args[0])
    if name == "__eventually":
        return "◇"+tel_label(args[0])
    if name == "__always":
        return "□"+tel_label(args[0])
    if name == "__until":
        return "("+tel_label(args[0])+" U "+tel_label(args[1])+")"
    if name == "__release":
        return "("+tel_label(args[0])+" R "+tel_label(args[1])+")"
    if name == "__and":
        return "("+tel_label(args[0])+" ∧ "+tel_label(args[1])+")"
    if name == "__or":
        return "("+tel_label(args[0])+" ∨ "+tel_label(args[1])+")"
    if name == "__neg":
        return "¬"+tel_label(args[0])
    else:
        return str(formula)

def get_tel_label(formula):
    return String(str(tel_label(formula)))

#end.
label(F,@get_tel_label(F)):-formula(tel,F).