Skip to content

Metric Equilibrium Logic (MEL)

A Metric Equilibrium Logic extension of ASP, using the clingcon system to handle the time aspect.

Usage

We can solve the metric problem from instances/paper-lights-constraint.lp with the following command:

> metasp solve clingcon  -c n=2 instances/paper-lights-constraint.lp --syntax-encoding syntax.lp --semantics-encoding semantics.lp  --printer mel_printer --python-scripts print_functions.py -n 0 --log warning
Metasp (<class 'clingcon.__main__.ClingconApp'>) version 5.2.1
Reading from instances/paper-lights-constraint.lp
Solving...
Answer: 1 (Time: 0.199s)
State 0  @0: light(l1) red(l1)
State 1  @5: light(l1) push(l1) red(l1)
State 2  @15: green(l1) light(l1)

Answer: 2 (Time: 0.199s)
State 0  @0: light(l1) red(l1)
State 1  @5: light(l1) push(l1) red(l1)
State 2  @16: green(l1) light(l1)

Answer: 3 (Time: 0.200s)
State 0  @0: light(l1) red(l1)
State 1  @5: light(l1) push(l1) red(l1)
State 2  @17: green(l1) light(l1)

Answer: 4 (Time: 0.200s)
State 0  @0: light(l1) red(l1)
State 1  @5: light(l1) push(l1) red(l1)
State 2  @18: green(l1) light(l1)

Answer: 5 (Time: 0.201s)
State 0  @0: light(l1) red(l1)
State 1  @5: light(l1) push(l1) red(l1)
State 2  @19: green(l1) light(l1)

SATISFIABLE

Models       : 5
Calls        : 1
Time         : 0.201s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.200s

Notice the use of a custom temporal printer that enhances the temporal printer with the time via @T.

UI

To run the UI use the following command:

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

Example

Traffic Lights

light(l1).
red(L) :- not green(L), light(L).
&eventually(&i(10,15),green(L)):- push(L).
&next(&i(5,6),push(l1)) :- &initial. %Here we limit the time for the next otherwise clingcon never shows models

Definition of the system

Configuration

syntax-encoding:
  - "./syntax.lp"
semantics-encoding:
  - "./semantics.lp"
printer: mel_printer
python-scripts:
  - "./print_functions.py"
ui-encoding:
  - "./ui.lp"
required-constants:
  - "n"
control-name: clingcon

Syntax

#type upper_bound {
  subtypes: {
    number;
    supremum;
  };
}.
#type interval {
  expressions: {
    &i/2: {
      type: number, safety: unsafe;
      type: upper_bound, safety: unsafe;
    };
  };
}.
#type mel {
  expressions: {
    &true/0;
    &false/0;
    &initial/0;
    &final/0;
    &next/2: {
      type: interval, safety: unsafe;
      type: mel, safety: safe;
    };
    &eventually/2: {
      type: interval, safety: unsafe;
      type: mel, safety: safe;
    };
    &always/2: {
      type: interval, safety: unsafe;
      type: mel, safety: unsafe;
    };
  };
  subtypes: {
    atom;
  };
  macros: {
    &next(v1): &next(&i(0, #sup), v1);
    where: {
      v1: mel;
    };
  };
  occurrence: any;
}.

Semantics

Uses the provided standard encodings:

semantics.lp

Encoding

Semantics encoding for Metric Equilibrium Logic (MEL)

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

&initial
true(&initial,0) :- formula(mel,&initial).
:- formula(mel,&initial), true(&initial,T), T!=0.
&next
true(F,T+1) : time(T+1) :- formula(mel,&next(I,F)), true(&next(I,F),T).
:- true(&next(I,_),T), outside(I,(T,T+1)), time(T).
true(&next(I,F),T) :- formula(mel,&next(I,F)), true(F,T+1), time(T), not outside(I,(T,T+1)).
&eventually
witness(eventually(I,F),(T,J)): time(J), T<=J :- true(&eventually(I,F),T).
true(&eventually(I,F),T) :- witness(eventually(I,F),(T,J)),
                           time(T), time(J), T<=J.
:- witness(eventually(I,F),(T,J)), outside(I,(T,J)),
                           time(T), time(J), T<=J.
true(F,J):-witness(eventually(I,F),(T,J)),
           time(T), time(J), T<=J.
witness(eventually(I,F),(T,J)):- formula(mel,&eventually(I,F)), true(F,J), not outside(I,(T,J)),
                                 time(T), time(J), T<=J.
&always
true(&always(I,F),T) :- witness(&always(I,F),(T,J)) : time(J), T<=J;
                       formula(mel, &always(I,F)), time(T).
witness(&always(I,F),(T,J)) :- true(&always(I,F),T),
                              time(T), time(J), T<=J.
witness(&always(I,F),(T,J)) :- outside(I,(T,J)), formula(mel, &always(I,F)),
                              time(T), time(J), T<=J.
witness(&always(I,F),(T,J)) :- true(F,J), formula(mel, &always(I,F)),
                              time(T), time(J), T<=J.
true(F,J) :- witness(&always(I,F),(T,J)), not outside(I,(T,J)),
             time(T), time(J), T<=J.
&final
:- true(&final,T), time(T), T!=n.
true(&final,n).
&true
true(&true,T) :- formula(mel,&true), time(T).
&false
:- formula(mel,&false), time(T), true(&false,T).

Time

&sum{t(0)} = 0 :- time(0).
&sum{t(T) ; -t(T+1)} <= -1:- time(T), time(T+1).

Intervals

i((M,N)) :- formula(mel, &eventually(&i(M,N),V)).
i((M,N)) :- formula(mel, &always(&i(M,N),V)).
i((M,N)) :- formula(mel, &next(&i(M,N),V)).
outside(&i(M,N),(T,T')):-
    i((M,N)), time(T), time(T'), T<=T', &sum{t(T); -t(T')} > -M.
outside(&i(M,N),(T,T')):-
    i((M,N)), time(T), time(T'), T<=T', &sum{t(T'); -t(T)} > N-1, N!=#sup.