### Telingo Command-Line Usage Source: https://github.com/potassco/telingo/blob/master/README.md Demonstrates basic command-line execution of the Telingo solver, including how to view help and run example programs. It highlights the `telingo` command and its arguments. ```bash telingo --help telingo examples/example1.lp ``` -------------------------------- ### Telingo Temporal Logic Example: Output with State Unfolding Source: https://github.com/potassco/telingo/blob/master/README.md Illustrates the output of Telingo when run with the `--imin=2` option, showing the step-by-step unfolding of states in a temporal program. It displays the initial state and subsequent states as the solver progresses. ```text Solving... Answer: 1 State 0: unloaded Solving... Answer: 1 State 0: unloaded State 1: shoot unloaded SATISFIABLE ``` -------------------------------- ### Telingo Temporal Logic Example: Basic Actions Source: https://github.com/potassco/telingo/blob/master/README.md A temporal logic program written for Telingo, demonstrating dynamic state transitions with actions like 'shoot', 'load', and 'wait'. It defines rules for updating 'loaded' and 'unloaded' states and includes an integrity constraint. ```asp #program dynamic. shoot | load | wait. loaded :- load. loaded :- 'loaded, not unloaded. unloaded :- shoot, 'loaded. unloaded :- 'unloaded, not loaded. :- load, 'loaded. #program initial. unloaded. ``` -------------------------------- ### Running Telingo from Source Source: https://github.com/potassco/telingo/blob/master/README.md Explains how to execute Telingo directly from its source code using Python's module execution. This is useful for development or when direct installation is not preferred. ```python python -m telingo ``` -------------------------------- ### Tower of Hanoi Example (Telingo/ASP) Source: https://context7.com/potassco/telingo/llms.txt Presents a planning problem for the Tower of Hanoi solved using Telingo with dynamic program parts. It includes rules for moving disks, effect propagation, frame axioms, and move validity checks, demonstrating temporal constraint solving. ```telingo # Program: examples/hanoi/encoding.lp #program dynamic. # Move a disk to some peg 1 {move(D,P) : _disk(D), _peg(P)} 1. move(D) :- move(D,P). # Effects of moves - on(D,P) holds if we move disk D to peg P on(D,P) :- move(D,P). # Frame axiom - disk stays if not moved on(D,P) :- 'on(D,P), not move(D). # Check moves validity blocked(D-1,P) :- 'on(D,P). blocked(D-1,P) :- blocked(D,P), _disk(D). # Cannot move if smaller disk blocks position :- move(D,P), blocked(D-1,P). # Cannot move disk if blocked where it currently is :- move(D), 'on(D,P), blocked(D,P). ``` -------------------------------- ### Dynamic Logic Formulas (Telingo/ASP) Source: https://context7.com/potassco/telingo/llms.txt Demonstrates the use of Dynamic Logic (DL) formulas in Telingo, employing path expressions and modalities. The example shows how to express conditions involving sequences of actions, such as eventually achieving a state 'b' after checking for 'a'. ```telingo # Program: examples/del/ex1.lp # Dynamic logic formula: <(a?;T)*>b # Meaning: eventually b after any sequence of checking a :- not &del{*(?a ;; &true) .>* b}. b. a. b'. # b holds in next state ``` -------------------------------- ### Execute Telingo Application with Command-Line Interface Source: https://context7.com/potassco/telingo/llms.txt Demonstrates using the telingo.TelApp class as a standalone solver with command-line arguments or programmatic control. The application manages incremental solving loops, registers temporal-specific options like --imin and --imax, and formats output by grouping atoms by state. ```Python from telingo import TelApp from clingo.application import clingo_main import sys app = TelApp() sys.exit(int(clingo_main(app, ["program.lp", "--imin=2"]))) from clingo import Control prg = Control() app.main(prg, ["examples/simple/encoding.lp", "examples/simple/instance.lp"]) ``` -------------------------------- ### Run Telingo from Command Line Source: https://context7.com/potassco/telingo/llms.txt Execute temporal logic programs using the Telingo solver via the command line. Options include specifying iteration steps, controlling stopping criteria, and running from source. Use '--help' for a full list of options. ```bash # Basic usage telingo examples/simple/encoding.lp examples/simple/instance.lp # Specify minimum and maximum iteration steps telingo --imin=2 --imax=10 program.lp # Control stopping criterion (sat, unsat, or unknown) telingo --istop=unsat program.lp # Run from source python -m telingo program.lp # Display help telingo --help ``` -------------------------------- ### ASP Constraints for Hanoi Tower Disk Management Source: https://context7.com/potassco/telingo/llms.txt Defines ASP constraints ensuring each disk exists on exactly one peg and verifies the goal state. The first constraint enforces cardinality constraints, the second checks goal conditions in non-testing mode, and the show directives specify which predicates to display in results. ```ASP :- _disk(D), not 1 {on(D,P)} 1. #program final. :- _goal_on(D,P), not on(D,P), not _testing. #show move/2. #show on/2. ``` -------------------------------- ### Temporal Atoms with Primes (Telingo/ASP) Source: https://context7.com/potassco/telingo/llms.txt Illustrates referencing past and future states using prime notation (') in atom names within Telingo programs. This allows reasoning about state transitions, such as 'loaded' referring to the previous state. ```telingo # Program: examples/simple/encoding.lp #program always. # Choose to either shoot or load the gun shoot | load. # Propagate action effects loaded :- load. unloaded :- shoot, not fail. # Frame axioms - 'loaded refers to previous state loaded :- 'loaded, not unloaded. unloaded :- 'unloaded, not loaded. # Program: examples/simple/instance.lp # initially the gun is unloaded unloaded. ``` -------------------------------- ### Transform Temporal Programs to Incremental ASP with Python Source: https://context7.com/potassco/telingo/llms.txt Converts temporal programs into incremental ASP programs with time parameters using the telingo.transformers module. It processes temporal rules, adds them to a Clingo control object via a program builder, and extracts future signatures and program parts for grounding and solving. ```Python from telingo.transformers import transform from clingo import ast, Control prg = Control() program = """ #program always. p :- 'q. p'. """ with ast.ProgramBuilder(prg) as bld: future_sigs, program_parts = transform([program], bld.add) prg.ground([("initial", []), ("always", [])]) prg.solve() ``` -------------------------------- ### Domain Generation for Temporal Logic Grounding - Telingo Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Generates auxiliary domains for grounding temporal logic atoms by collecting positive occurrences and associating time step ranges. Uses step predicates and choice rules to instantiate necessary parts of auxiliary programs. ```telingo #program initial. s(0). #program dynamic. s(S) :- s(S-1). #program always. #external go. H(T) :- 'H(T). { a } :- go, H(T), s(S), S+1 <= T, T < S+2. { b } :- go, H(T), s(S), S+1 <= T. { c } :- go, H(T), s(S), S <= T, T < S+1. ``` -------------------------------- ### Telingo Path Expressions: Syntax and Operators Source: https://github.com/potassco/telingo/blob/master/README.md Details the syntax for constructing path expressions in Telingo's dynamic logic. It covers Kleene star (*), test (?), disjunction (+), sequence (;;), and the true literal (&true). Path expressions must be in normal form. ```telingo # Example: &del{*(?a ;; &true) .>? b} for <(a?;T)*>b # Example: &del{?a + ?b .>* c} for [a?+b?]c ``` -------------------------------- ### Temporal Operators Reference for Rule Bodies and Heads Source: https://context7.com/potassco/telingo/llms.txt Complete reference of temporal operators supported in telingo including boolean operators (conjunction, disjunction, negation, implications), past operators (previous, weak previous, trigger, since), future operators (next, weak next, release, until), and special formulas (true, false, initial, final, initially, finally). Dynamic logic operators are also supported. ```ASP &tel { a & b } &tel { a | b } &tel { ~ a } &tel { a <- b } &tel { a -> b } &tel { a <> b } &tel { < a } &tel { <: a } &tel { a <* b } &tel { <* b } &tel { a a } &tel { >: a } &tel { a >* b } &tel { >* b } &tel { a >? b } &tel { >? b } &tel { a ;> b } &tel { a ;>: b } &tel { &true } &tel { &false } &tel { &initial } &tel { &final } &tel { << p } &tel { >> p } &del { p .>* q } &del { p .>? q } &del { * ?a } &del { ?a + ?b } &del { p ;; q } ``` -------------------------------- ### Telingo Output: Gun Breakage Simulation Source: https://github.com/potassco/telingo/blob/master/README.md This is the output from running the Telingo program for gun breakage. It shows the solving process and the resulting stable models (states) of the system, illustrating the gun's behavior and breakage over time. ```text Solving... Solving... Solving... Solving... Solving... Answer: 1 State 0: unloaded State 1: shoot unloaded State 2: broken shoot unloaded State 3: broken load loaded State 4: broken loaded shoot SATISFIABLE ``` -------------------------------- ### Telingo Main Solving Loop Function (Python) Source: https://context7.com/potassco/telingo/llms.txt Demonstrates the core incremental solving loop in Python using Telingo's `imain` function. It handles time step unfolding and future atom management, requiring the `clingo` library. The `on_model` callback processes solutions at each step. ```python from telingo import imain import clingo # Define a simple on_model callback def on_model(model, step): print(f"Solution at step {step}:") for symbol in model.symbols(shown=True): print(f" {symbol}") # Create control object and ground program prg = clingo.Control() prg.add("base", [], "p.") prg.ground([("base", [])]) # Run incremental solving future_sigs = [("__future_p", 2, True)] # Future signatures to constrain program_parts = [("always", "always", range(1))] # Parts to ground imain(prg, future_sigs, program_parts, on_model, imin=0, imax=5, istop="SAT") ``` -------------------------------- ### Linear Temporal Logic Formulas (Telingo/ASP) Source: https://context7.com/potassco/telingo/llms.txt Shows how to incorporate Linear Temporal Logic (LTL) formulas using temporal operators within theory atoms in Telingo. This enables expressing complex temporal relationships like eventualities and past conditions. ```telingo # Program with LTL formulas #program always. shoot | load. loaded :- load. unloaded :- shoot, not fail. loaded :- 'loaded, not unloaded. unloaded :- 'unloaded, not loaded. # Eventually fail if two shots without loading # shoot & < ? fail } :- not not &tel { shoot & < q }.") prg.ground([("base", [Number(0)])]) horizon = 0 thy.translate(horizon, prg) prg.ground([("base", [Number(1)])]) horizon = 1 thy.translate(horizon, prg) ``` -------------------------------- ### Program Part Directives (Telingo/ASP) Source: https://context7.com/potassco/telingo/llms.txt Explains how to use special program parts (`initial`, `always`, `dynamic`, `final`) in Telingo to control the scope and timing of rules. Each part specifies when a set of rules is applied during the temporal unfolding. ```telingo # initial: applies only to first state (step 0) #program initial. unloaded. # always: applies to all states (step >= 0) #program always. shoot | load. loaded :- 'loaded, not unloaded. # dynamic: applies to all states except first (step > 0) #program dynamic. move(D,P) :- on(D,P). on(D,P) :- 'on(D,P), not move(D). # final: applies only to last state #program final. :- not goal_achieved. ``` -------------------------------- ### Telingo Dynamic Logic: Box and Diamond Operators Source: https://github.com/potassco/telingo/blob/master/README.md Explains the usage of dynamic logic operators in Telingo, specifically the box (always) and diamond (eventually) operators, represented as .>* and .>? respectively. These operators are used within dynamic formulas in constraints and theory atoms. ```telingo #program dynamic. # ... other rules ... broken :- shoot, not not &tel { <* unloaded & < *(~loaded | ~shoot) }. ``` -------------------------------- ### Auxiliary Predicate Rewriting for Temporal Logic - Telingo Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Demonstrates rewriting original rules with temporal logic heads into auxiliary predicates. The auxiliary predicate captures the body conditions with time steps, enabling later propositional-level translation. ```telingo H(T) :- B, s(T). > (a & >* b) & c :- H(T). ``` -------------------------------- ### Telingo Program: Gun Breakage Logic Source: https://github.com/potassco/telingo/blob/master/README.md This Telingo program defines rules for a gun's state, including loading, shooting, and breaking. It encodes the condition that the gun breaks if it's shot twice without reloading and selects traces where the gun did not shoot because it broke. It utilizes dynamic logic features for state transitions. ```telingo #program dynamic. shoot | load | wait. loaded :- load. loaded :- 'loaded, not unloaded. unloaded :- shoot, 'loaded, not broken. unloaded :- 'unloaded, not loaded. :- load, 'loaded. broken :- shoot, not not &tel { <* unloaded & < *(~loaded | ~shoot) }. ``` -------------------------------- ### Until Operator Translation - Telingo Temporal Logic Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Translates the until operator (&tel { a >? b }) by unpacking for multiple steps. Shows the equivalent disjunctive rules that capture the semantics across time steps. ```telingo #program initial. &tel { a >? b }. #program dynamic. c :- 'c. c :- 'b. #program always. b | a :- not c. b :- not c, not &tel { > (a >? b) }. ``` -------------------------------- ### Next Operator Translation - Telingo Temporal Logic Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Translates the next operator (&tel { n > a }) into an equivalent program preserving derivation for 'a'. The translation uses step counters and auxiliary predicates to handle time-dependent constraints. Applies to both classical next and weak next (>) operators. ```telingo #program initial. &tel { n > a }. #program always. a :- n - __t + s == 0. :- not &tel { (n - __t + s) > a }, n - __t + s > 0. :- not &tel { (__t - s - n) < a }, n - __t + s < 0. ``` -------------------------------- ### Release Operator Translation - Telingo Temporal Logic Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Translates the release operator (&tel { a >* b }) by unpacking across multiple time steps. Generates constraints and rules for each step using auxiliary predicates and negation. ```telingo #program initial. &tel { a >* b }. #program dynamic. c :- 'c. c :- 'a. #program always. b :- not c. a :- not c, not &tel { > (a >* b) }. ``` -------------------------------- ### Eventually Operator Translation - Telingo Temporal Logic Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Translates the eventually operator (&tel { >? (a & b) }) into a dynamic program with recursive rules and integrity constraints. Uses auxiliary predicates to track occurrence and combine with negation-as-failure. ```telingo #program initial. &tel { >? (a & b) }. #program dynamic. c :- 'c. c :- 'a, 'b. #program always. b :- not c, not &tel { > >? (a & b) }. ``` -------------------------------- ### Always Operator Translation - Telingo Temporal Logic Source: https://github.com/potassco/telingo/blob/master/doc/translation.md Translates the always operator (&tel { >* (a | b) }) into the simplest equivalent form. Preserves strong equivalence and only requires shifting for disjunctions. ```telingo #program initial. &tel { >* (a | b) }. #program always. a | b. ``` === COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.