diff --git a/.gitignore b/.gitignore index 59ddbcb..a1b9add 100644 --- a/.gitignore +++ b/.gitignore @@ -34,3 +34,5 @@ build .coverage _build _autosummary + +out \ No newline at end of file diff --git a/examples/telingo/lights/README.md b/examples/telingo/lights/README.md new file mode 100644 index 0000000..c0a27f4 --- /dev/null +++ b/examples/telingo/lights/README.md @@ -0,0 +1,77 @@ +# Telingo example + +## Basic usage + +### Input + +``` +next(push) :- initially. + +:- red, green. +red :- not green. +next(next(green)):- push. +red :- prev(green), prev(prev(green)). +``` + +### Output + +```shell +renopro reify examples/telingo/lights/instance.lp | renopro transform --meta-encoding examples/telingo/transformer.lp --input-format=reified --clingo-options -c horizon=6 > examples/telingo/lights/final.lp +``` + +``` +#program base. +push((T+1)) :- initially(T); time(T). +#false :- red(T); green(T); time(T). +red(T) :- not green(T); time(T). +green((T+2)) :- push(T); time(T). +red(T) :- green((T-1)); green((T-2)); time(T). +time(0). +time(1). +time(2). +time(3). +time(4). +time(5). +time(6). +initially(0). +finally(6). +``` + +### Run clingo to get a plan + +```shell +clingo examples/telingo/lights/final.lp +``` +``` +pyclingo version 5.6.2 +Reading from examples/telingo/lights/final.lp +Solving... +Answer: 1 +time(0) time(1) time(2) time(3) time(4) time(5) time(6) initially(0) push(1) green(3) red(0) red(1) red(2) red(4) red(5) red(6) finally(6) +SATISFIABLE + +Models : 1+ +Calls : 1 +Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) +CPU Time : 0.000s +``` + + + +## Visualize instance + + +```shell +renopro reify examples/telingo/lights/instance.lp | clingraph --viz src/renopro/asp/viz.lp --out=render --view --format png --name-format="instance" --dir=examples/telingo/lights +``` + +![](instance.png) + +## Visualize result after transformation + +```shell +renopro reify examples/telingo/lights/instance.lp | renopro transform --meta-encoding examples/telingo/transformer.lp --input-format=reified --output-format=reified --clingo-options -c horizon=6 | clingraph --viz src/renopro/asp/viz.lp --out=render --view --format png --name-format="final" --dir=examples/telingo/lights +``` + + +![](final.png) diff --git a/examples/telingo/lights/final.lp b/examples/telingo/lights/final.lp new file mode 100644 index 0000000..35a074a --- /dev/null +++ b/examples/telingo/lights/final.lp @@ -0,0 +1,9 @@ +#program base. +push((T+1)) :- initially(T); time(T). +#false :- red(T); green(T); time(T). +red(T) :- not green(T); time(T). +green((T+2)) :- push(T); time(T). +red(T) :- green((T-1)); green((T-2)); time(T). +time((0..6)). +initially(0). +finally(6). diff --git a/examples/telingo/lights/final.png b/examples/telingo/lights/final.png new file mode 100644 index 0000000..ebf81ea Binary files /dev/null and b/examples/telingo/lights/final.png differ diff --git a/examples/telingo/lights/instance.lp b/examples/telingo/lights/instance.lp new file mode 100644 index 0000000..03e2d96 --- /dev/null +++ b/examples/telingo/lights/instance.lp @@ -0,0 +1,6 @@ +next(push) :- initially. + +:- red, green. +red :- not green. +next(next(green)):- push. +red :- prev(green), prev(prev(green)). \ No newline at end of file diff --git a/examples/telingo/lights/instance.png b/examples/telingo/lights/instance.png new file mode 100644 index 0000000..64fb732 Binary files /dev/null and b/examples/telingo/lights/instance.png differ diff --git a/examples/telingo/simple/README.md b/examples/telingo/simple/README.md new file mode 100644 index 0000000..3f62c61 --- /dev/null +++ b/examples/telingo/simple/README.md @@ -0,0 +1,43 @@ +# Telingo example + +## Basic usage + +### Input + +``` +a:- prev(a). +next(b):- b. +``` + +### Output + +```shell +renopro reify examples/telingo/simple/instance.lp | renopro transform --meta-encoding examples/telingo/transformer.lp --input-format=reified > examples/telingo/simple/final.lp +``` + +``` +#program base. +a(T) :- a((T-1)); time(T). +b((T+1)) :- b(T); time(T). +time((0..1)). +initially(0). +finally(1). +``` + +## Visualize instance + + +```shell +renopro reify examples/telingo/simple/instance.lp | clingraph --viz src/renopro/asp/viz.lp --out=render --view --format png --name-format="instance" --dir=examples/telingo/simple +``` + +![](instance.png) + +## Visualize result after transformation + +```shell +renopro reify examples/telingo/simple/instance.lp | renopro transform --meta-encoding examples/telingo/transformer.lp --input-format=reified --output-format=reified | clingraph --viz src/renopro/asp/viz.lp --out=render --view --format png --name-format="final" --dir=examples/telingo/simple +``` + + +![](final.png) diff --git a/examples/telingo/simple/final.lp b/examples/telingo/simple/final.lp new file mode 100644 index 0000000..d207bb4 --- /dev/null +++ b/examples/telingo/simple/final.lp @@ -0,0 +1,6 @@ +#program base. +a(T) :- a((T-1)); time(T). +b((T+1)) :- b(T); time(T). +time((0..1)). +initially(0). +finally(1). diff --git a/examples/telingo/simple/final.png b/examples/telingo/simple/final.png new file mode 100644 index 0000000..b7a30f9 Binary files /dev/null and b/examples/telingo/simple/final.png differ diff --git a/examples/telingo/simple/instance.lp b/examples/telingo/simple/instance.lp new file mode 100644 index 0000000..73a7dde --- /dev/null +++ b/examples/telingo/simple/instance.lp @@ -0,0 +1,2 @@ +a:- prev(a). +next(b):- b. \ No newline at end of file diff --git a/examples/telingo/simple/instance.png b/examples/telingo/simple/instance.png new file mode 100644 index 0000000..53f8c00 Binary files /dev/null and b/examples/telingo/simple/instance.png differ diff --git a/examples/telingo/transformer.lp b/examples/telingo/transformer.lp new file mode 100644 index 0000000..4c08e99 --- /dev/null +++ b/examples/telingo/transformer.lp @@ -0,0 +1,124 @@ +#const horizon = 1. + + +% auxiliary atoms +max_arg_index(TT,Idx) + :- Idx = #max{ Pos : terms(TT,Pos,_); -1 }, function(_,_,terms(TT)). + +max_lit_index(LT,Idx) + :- Idx = #max{ P : body_literals(LT,P,_); -1 }, rule(_,_,body_literals(LT)). + +max_statement_index(S,Idx) + :- Idx = #max{ P : statements(S,P,_); -1 }, + program("base",_,statements(S)). + + +arity(F,N+1) :- function(F,_,terms(T)), max_arg_index(T,N). + +% chain modal operators +modal(prev). +modal(next). +% modal(initially). + +chain(M,A,function(F),O) + :- symbolic_atom(A,function(F)), function(F,M,terms(T)), arity(F,1), + terms(T,0,O), + modal(M). + +chain(M,A,function(F),O) + :- chain(M,A,_,function(F)), function(F,M,terms(T)), arity(F,1), + terms(T,0,O), + modal(M). + +% final operand must be a constant or function, as e.g. prev(1) is not a prev operation +final_operand(A,O) + :- chain(M,A,F,O), not chain(M,A,O,_), + O=function(_), + modal(M). + +num(M,A,N) :- N = #count{ F : chain(M,A,F,_) }, chain(M,A,_,_). + +first(M,A,F) :- chain(M,A,F,O), not chain(M,A,_,F). + + +% ----- Prop +ast_operation( + add(variable(time_variable(term(T)),"T"); + terms(T,N+1,variable(time_variable(term(T)))))) + :- symbolic_atom(A,function(F)), function(F,Name,terms(T)), + not modal(Name), max_arg_index(T,N). + +% ----- Prev +ast_operation( + delete(function(F,N,T1)); + add(function(F,Name,terms(T2)); + variable(time_variable(function(F)),"T"); + terms(T2,I+1,binary_operation(new_id(O))); + binary_operation(new_id(O),"-",variable(time_variable(function(F))),number(new_id(O))); + number(new_id(O),Num))) +:- first(prev,A,function(F)), function(F,N,T1), final_operand(A,function(O)), + function(O,Name,terms(T2)), max_arg_index(T2,I), num(prev,A,Num). + +% ----- Next +ast_operation( + delete(function(F,N,T1)); + add(function(F,Name,terms(T2)); + variable(time_variable(function(F)),"T"); + terms(T2,I+1,binary_operation(new_id(O))); + binary_operation(new_id(O),"+",variable(time_variable(function(F))),number(new_id(O))); + number(new_id(O),Num))) +:- first(next,A,function(F)), function(F,N,T1), final_operand(A,function(O)), + function(O,Name,terms(T2)), max_arg_index(T2,I), num(next,A,Num). + +% ----- Time steps as new fact with interval 0..horizon +ast_operation( + add(number(time_number_0,0)); + add(number(time_number_h,horizon)); + add(interval(time_interval,number(time_number_0),number(time_number_h))); + add(terms(time_terms,0,interval(time_interval))); + add(function(time_function,time,terms(time_terms))); + add(symbolic_atom(time_symbol,function(time_function))); + add(literal(time_literal,"pos",symbolic_atom(time_symbol))); + add(rule(time_rule,literal(time_literal),body_literals(time_body_literals)))). + +ast_operation(add(statements(S,X+1,rule(time_rule)))) + :- program("base",_,statements(S)), max_statement_index(S,X). + +% Add time(T) in all rules +ast_operation( + add(variable(time_variable(R),"T")); + add(terms(time_terms_var(R),0,variable(time_variable(R)))); + add(function(time_function_var(R),time,terms(time_terms_var(R)))); + add(symbolic_atom(time_symbol_var(R),function(time_function_var(R)))); + add(body_literal(time_body_literal_var(R),"pos",symbolic_atom(time_symbol_var(R)))); + add(body_literals(B,MAX+1,body_literal(time_body_literal_var(R)))) + ) +:- rule(R,_,body_literals(B)), max_lit_index(B,MAX). + +% Add initially(0). +ast_operation( + add(number(init_number,0)); + add(terms(init_terms,0,number(init_number))); + add(function(init_function,initially,terms(init_terms))); + add(symbolic_atom(init_symbol,function(init_function))); + add(literal(init_literal,"pos",symbolic_atom(init_symbol))); + add(rule(init_rule,literal(init_literal),body_literals(init_body_literals)))). + +ast_operation(add(statements(S,X+2,rule(init_rule)))) + :- program("base",_,statements(S)), max_statement_index(S,X). + + + +% Add finally(horizon). +ast_operation( + add(number(final_number,horizon)); + add(terms(final_terms,0,number(final_number))); + add(function(final_function,finally,terms(final_terms))); + add(symbolic_atom(final_symbol,function(final_function))); + add(literal(final_literal,"pos",symbolic_atom(final_symbol))); + add(rule(final_rule,literal(final_literal),body_literals(final_body_literals)))). + +ast_operation(add(statements(S,X+3,rule(final_rule)))) + :- program("base",_,statements(S)), max_statement_index(S,X). + + diff --git a/examples/test.lp b/examples/test.lp new file mode 100644 index 0000000..2f34e39 --- /dev/null +++ b/examples/test.lp @@ -0,0 +1,7 @@ +% {_r(X):X=1..3}. +% :- not _r(X), X=1..3. + + +b(1):- _r(1). +c(2):- _r(2). +a :- b(X), c(X), _r(3). \ No newline at end of file diff --git a/examples/test_fo.lp b/examples/test_fo.lp new file mode 100644 index 0000000..e69de29 diff --git a/examples/test_go.lp b/examples/test_go.lp new file mode 100644 index 0000000..8ed4647 --- /dev/null +++ b/examples/test_go.lp @@ -0,0 +1,2 @@ +b(1). +c(2). diff --git a/src/renopro/asp/viz.lp b/src/renopro/asp/viz.lp new file mode 100644 index 0000000..6c8b9d6 --- /dev/null +++ b/src/renopro/asp/viz.lp @@ -0,0 +1,122 @@ +#include "defined.lp". +#const pos_body_lit_color= "#B5D99C". +#const neg_body_lit_color= "#D9A69C". +#const tab_color= "#E0E0C8". +#const program_color = "#A4C9DE". +#const rule_color = "#C8D7E0". + +node(N2):-edge((N1,N2)). +% attr(node,N,label,"test") :- node(N). +attr(node,N,label,"<{{name}}{% if value is defined %}

{{value}} {% else %} {% endif %}>") :- node(N). +attr(node,N,(label,name),N) :- node(N). +attr(node,N,style,filled) :- node(N), not attr(node,N,shape,plaintext). +attr(edge,(N1,N2),fontsize,8):-edge((N1,N2)). + + +node(string(Id)) :- string(Id,Val). +attr(node,string(Id),(label,value),Val) :- string(Id,Val). +attr(node,string(Id),shape,plaintext) :- string(Id,Val). + +node(number(Id)) :- number(Id,Val). +attr(node,number(Id),(label,value),Val) :- number(Id,Val). +attr(node,number(Id),shape,plaintext) :- number(Id,Val). + + +node(variable(Id)) :- variable(Id,Name). +attr(node,variable(Id),(label,value),Name) :- variable(Id,Name). +attr(node,variable(Id),shape,plaintext) :- node(variable(Id)). + +% node(unary_operation(Id)) :- unary_operation(Id,Operator,Argument). +node(binary_operation(Id)) :- binary_operation(Id,Operator,Left,Right). +attr(node,binary_operation(Id),shape,cds) :- binary_operation(Id,Operator,Left,Right). +attr(node,binary_operation(Id),(label,value),Operator) :- binary_operation(Id,Operator,Left,Right). +edge((binary_operation(Id),Left)) :- binary_operation(Id,Operator,Left,Right). +attr(edge,(binary_operation(Id),Left),label,left) :- binary_operation(Id,Operator,Left,Right). +edge((binary_operation(Id),Right)) :- binary_operation(Id,Operator,Left,Right). +attr(edge,(binary_operation(Id),Right),label,right) :- binary_operation(Id,Operator,Left,Right). + + +node(interval(Id)) :- interval(Id,Left,Right). +attr(node,interval(Id),shape,trapezium) :- interval(Id,Left,Right). +edge((interval(Id),Left)) :- interval(Id,Left,Right). +attr(edge,(interval(Id),Left),label,left) :- interval(Id,Left,Right). +edge((interval(Id),Right)) :- interval(Id,Left,Right). +attr(edge,(interval(Id),Right),label,right) :- interval(Id,Left,Right). + +node(terms(Id)) :- terms(Id,Pos,Element). +attr(node,terms(Id),shape,tab) :- node(terms(Id)). +attr(node,terms(Id),fillcolor,tab_color) :- node(terms(Id)). +edge((terms(Id),Element)) :- terms(Id,Pos,Element). +attr(edge,(terms(Id),Element),label,Pos) :- terms(Id,Pos,Element). + +node(function(Id)) :- function(Id,Name,Args). +edge((function(Id),Args)) :- function(Id,Name,Args). +attr(node,function(Id),(label,value),Name) :- function(Id,Name,Args). +attr(node,function(Id),shape,plaintext) :- function(Id,Name,Args). + +% node(pool(Id)) :- pool(Id,Args). +% node(guard(Id)) :- guard(Id,Op,Term). +% node(guards(Id)) :- guards(Id,Pos,Element). +% node(comparison(Id)) :- comparison(Id,Guards). +% node(boolean_constant(Id)) :- boolean_constant(Id,Bool). + +node(symbolic_atom(Id)) :- symbolic_atom(Id,Symbol). +attr(node,symbolic_atom(Id),shape,box) :- symbolic_atom(Id,Symbol). +edge((symbolic_atom(Id),Symbol)) :- symbolic_atom(Id,Symbol). + +node(literal(Id)) :- literal(Id,Sign,Atom). +attr(node,literal(Id),fillcolor,pos_body_lit_color) :- literal(Id,"pos",Atom). +attr(node,literal(Id),fillcolor,neg_body_lit_color) :- literal(Id,"not",Atom). +edge((literal(Id),Atom)) :- literal(Id,Sign,Atom). + +node(literals(Id)) :- literals(Id,Pos,Element). +attr(node,literals(Id),shape,tab) :- node(literals(Id)). +attr(node,literals(Id),fillcolor,tab_color) :- node(literals(Id)). +edge((literals(Id),Element)) :- literals(Id,Pos,Element). +attr(edge,(literals(Id),Element),label,pos) :- literals(Id,Pos,Element). + +% node(conditional_literal(Id)) :- conditional_literal(Id,Literal,Condition). +% node(agg_elements(Id)) :- agg_elements(Id,Pos,Element). +% node(aggregate(Id)) :- aggregate(Id,LGuard,Elements,RGuard). +% node(body_agg_elements(Id)) :- body_agg_elements(Id,Pos,Terms,Condition). +% node(body_aggregate(Id)) :- body_aggregate(Id,LGuard,Elements,RGuard). + +node(body_literal(Id)) :- body_literal(Id,Sign,Atom). +attr(node,body_literal(Id),fillcolor,pos_body_lit_color) :- body_literal(Id,"pos",Atom). +attr(node,body_literal(Id),fillcolor,neg_body_lit_color) :- body_literal(Id,"not",Atom). +edge((body_literal(Id),Atom)) :- body_literal(Id,Sign,Atom). + +node(body_literals(Id)) :- body_literals(Id,Pos,Element). +attr(node,body_literals(Id),shape,tab) :- node(body_literals(Id)). +attr(node,body_literals(Id),fillcolor,tab_color) :- node(body_literals(Id)). +edge((body_literals(Id),Element)) :- body_literals(Id,Pos,Element). +attr(edge,(body_literals(Id),Element),label,Pos) :- body_literals(Id,Pos,Element). + + +% node(head_agg_elements(Id)) :- head_agg_elements(Id,Pos,Terms,Condition). +% node(head_aggregate(Id)) :- head_aggregate(Id,LGuard,Elements,RGuard). +% node(disjunction(Id)) :- disjunction(Id,Pos,Element). + +node(rule(Id)) :- rule(Id,Head,Body). +attr(node,rule(Id),shape,rectangle) :- rule(Id,Head,Body). +attr(node,rule(Id),fillcolor,rule_color) :- rule(Id,Head,Body). +edge((rule(Id),Head)) :- rule(Id,Head,Body). +attr(edge,(rule(Id),Head),label,head) :- rule(Id,Head,Body). +edge((rule(Id),Body)) :- rule(Id,Head,Body). +attr(edge,(rule(Id),Body),label,body) :- rule(Id,Head,Body). + + +% node(constants(Id)) :- constants(Id,Pos,Element). + +node(program(Name)) :- program(Name,Params,Statements). +attr(node,program(Name),shape,invhouse) :- program(Name,Params,Statements). +attr(node,program(Name),fillcolor,program_color) :- program(Name,Params,Statements). +edge((program(Name),Statements)) :- program(Name,Params,Statements). + +node(statements(Id)) :- statements(Id,Pos,Element). +attr(node,statements(Id),shape,tab) :- node(statements(Id)). +attr(node,statements(Id),fillcolor,tab_color) :- node(statements(Id)). +edge((statements(Id),Element)) :- statements(Id,Pos,Element). +attr(edge,(statements(Id),Element),label,Pos) :- statements(Id,Pos,Element). + +% node(external(At)) :- external(Atom,Body,Type).