Dynamic Equilibrium Logic (DEL)¶

A Dynamic 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 5 which alternates green and red using the del extension:

> metasp solve clingo --meta-config config.yml -c n=4 instances/paper-lights.lp
Metasp (<class 'metasp.app.ClingoApp'>) version 5.8.0
Reading from instances/paper-lights.lp
Solving...
Answer: 1 (Time: 0.621s)
 State 0: green(l1) light(l1)
 State 1: light(l1) red(l1)
 State 2: green(l1) light(l1)
 State 3: light(l1) red(l1)
 State 4: light(l1)

SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 0.621s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.611s

UI¶

To run the UI use the following command:

metasp ui --meta-config config.yml -c n=4 instances/paper-lights.lp

Example¶

Traffic Lights

light(l1).
&eventually(&star(&seq(green(L),red(L))), &final) :-&initial, light(L).

Definition of the system¶

Configuration¶

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

Syntax¶

#type del{
  expressions: {
    &always/2: {
      type: path, safety: unsafe;
      type: del, safety: unsafe;
    };
    &eventually/2: {
      type: path, safety: safe;
      type: del, safety: safe;
    };
  };
  subtypes:  { tel; };
  occurrence: any;
}.

#type path {
  expressions: {
    &step/0;
    &test/1: { type: del, safety: safe; };
    &star/1: { type: path, safety: unsafe;};
    &choice/2: {
      type: path, safety: unsafe;
      type: path, safety: unsafe;
    };
    &seq/2: {
      type: path, safety: safe;
      type: path, safety: safe;
    };
  };
  macros: {
    a: &seq(&test(a), &step);
    where: { a: atom; };
  };
}.

Semantics¶

Uses the provided standard encodings:

meta-time.lp for the meta predicates with time support.
show-time.lp for the show predicates with time support.
reify-defined.lp to avoid warnings for the reification predicates.

`semantics.lp` ¶

Encoding

Operators¶

`&eventually(&step,_)`¶

true(F,K+1): time(K+1) :- formula(del,&eventually(&step,F)), true(&eventually(&step,F),K).
true(&eventually(&step,F),K) :- true(F,K+1), formula(del,&eventually(&step,F)), time(K).

`&eventually(&test,_)`¶

true(F,K) :- formula(del,&eventually(&test(F2),F)), true(&eventually(&test(F2),F),K).
true(F2,K) :- formula(del,&eventually(&test(F2),F)), true(&eventually(&test(F2),F),K).
true(&eventually(&test(F2),F),K) :- true(F,K),true(F2,K), formula(del,&eventually(&test(F2),F)).

%### `&eventually(&choice,_)`
true(&eventually(P1,F),K);true(&eventually(P2,F),K) :- true(&eventually(&choice(P1,P2),F),K).
true(&eventually(&choice(P1,P2),F),K) :- true(&eventually(P1,F),K), formula(del,&eventually(&choice(P1,P2),F)).
true(&eventually(&choice(P1,P2),F),K) :- true(&eventually(P2,F),K), formula(del,&eventually(&choice(P1,P2),F)).

%### `&eventually(&seq,_)`
true(&eventually(P1,&eventually(P2,F)),K) :- true(&eventually(&seq(P1,P2),F),K).
true(&eventually(&seq(P1,P2),F),K):- true(&eventually(P1,&eventually(P2,F)),K), formula(del, &eventually(&seq(P1,P2),F)).

%### `&eventually(&star,_)`
true(F,K); true(&eventually(P,&eventually(&star(P),F)),K):-  true(&eventually(&star(P),F),K).
true(&eventually(&star(P),F),K):-  formula(del, &eventually(&star(P),F)), true(F,K).
true(&eventually(&star(P),F),K):-  formula(del, &eventually(&star(P),F)), true(&eventually(P,&eventually(&star(P),F)),K).

%### `&always(&step,_)`
true(F,K+1):- formula(del,&always(&step,F)), true(&always(&step,F),K), time(K+1).
true(&always(&step,F),K) :- true(F,K+1), formula(del,&always(&step,F)), time(K).
true(&always(&step,F),K) :- formula(del,&always(&step,F)), time(K), not time(K+1).

`&always(&test,_)`¶

true(F,K) :- formula(del,&always(&test(F2),F)), true(&always(&test(F2),F),K), true(F2,K).

Maybe there is something missing here because implications in HT are different

true(&always(&test(F2),F),K) :- not true(F2,K), formula(del,&always(&test(F2),F)), time(K).
true(&always(&test(F2),F),K) :- true(F2,K), true(F,K), formula(del,&always(&test(F2),F)).


%### `&always(&choice,_)`
true(&always(P1,F),K) :- true(&always(&choice(P1,P2),F),K).
true(&always(P2,F),K) :- true(&always(&choice(P1,P2),F),K).
true(&always(&choice(P1,P2),F),K) :- true(&always(P1,F),K), true(&always(P2,F),K), formula(del,&always(&choice(P1,P2),F)).

%### `&always(&seq,_)`
true(&always(P1,&always(P2,F)),K) :- true(&always(&seq(P1,P2),F),K).
true(&always(&seq(P1,P2),F),K):- true(&always(P1,&always(P2,F)),K), formula(del, &always(&seq(P1,P2),F)).

%### `&always(&star,_)`
true(F,K):-  true(&always(&star(P),F),K).
true(&always(P,&always(&star(P),F)),K):-  true(&always(&star(P),F),K).
true(&always(&star(P),F),K):-  formula(del, &always(&star(P),F)), true(F,K), true(&always(P,&always(&star(P),F)),K).