By http://logicalcontracts.com, November 6, 2017
This document summarizes the Logical Contracts proprietary extensions to the Logic Production Systems described in http://lps.doc.ic.ac.uk. The system can be tried online at http://demo.logicalcontracts.com. Start by the Examples menu.
real_time(RT) at T
System fluent that returns the real time (seconds since Jan 1, 1970) at the begin of LPS cycle T.
Timeless predicate that returns the (real) time when the LPS execution began.
Time limit for the LPS program to execute. If maxTime(NumCycles) is also present, the earliest will cause the program to terminate.
lps_terminate from T1
System action that gracefully finishes the program.
This section introduces background processing for LPS on SWI Prolog (barebones). SWISH/web functionaly comes next below.
In what follows we distinguish a LPS program (the source code) from an execution of it (of which there may be several).
Causes the LPS interpreter to launch a new SWI Prolog thread executing the given program. When used in
golps(File,[...,background(ID),...]) etc. will cause this predicate to return immediately, binding ID to a token denoting the new LPS program execution thread.
Add a fixed "sleep" time to the program execution at the begin of each cycle, for the sake of the server environment.
Inject all events into the LPS server thread, after inserting whatever observations are declared for the program. See interpreter:updateEvents/3.
Result = ok(InsertionCycle); else, e.g. if some event violates the program integrity constraints, all events are rejected and `
Result = failed(Cause)
Fetches current values for all templates in Fluents into Values. Returns also the Cycle at which the values were samples. See answerthreadqueries/1.
The following "system actions" are provided by the LPS interpreter, and require the dc option.
lps_ask(ID,Events) from T1 to T2
Send all Events to the program execution ID, and wait for the events to be consumed - failing if they're not (say, because they violate ID's program constraints). Notice that this effectively hangs the LPS interpreter (for the current program) until the events are processed by ID - thus to use with care.
This is defined internally by the sequence of the next two actions.
lps_ask(ID,Events,MessageID) from T1 to T2
Send all Events to the program execution ID, succeeding immediately and returning a unique token MessageID, that can be used to find whether the events are accepted.
lps_outcome(MessageID,Result) from T3 to T4
Find out whether events sent by the previous action (denoted by MessageID) were accepted by the destinatary LPS program execution. lps_outcome will be delayed until the events were processed, and will return Result=ok(InsertionCycle) or Result=failure(Cause).
The above features are made available in the LPS web server (swish, currently at http://lcdemo.logicalcontracts.com) via the following new predicates and web services. This brings LPS into new territory, and server operation challenges.
To minimize server load, LPS programs are obliged to declare a minimum cycle sleep time with minCycleTime(Min), currently Min >= 0.1 mS. LPS server executions will be aborted if the expected load per user (or in the whole system) is too big (see checkuserserverusage in logicalcontracts/lc/lpsserver_UI.pl).
For use in the SWISH goal field.
Executes in background the LPS program in the current editor window. ID is bound to a thread identifier, unique in the running SWI Prolog/SWISH server. A term renderer is used to display a link to the "LPS manager" page for the new LPS execution.
Shows links to managers for all running LPS programs of the current user.
Shows all LPS program threads IDs, even after they're finished.
Brutal cleanup, kills LPS programs of all users.
The LPS manager page shows the current status of the LPS server program, including real time global attributes. In addition it provides links to inspect current state of all fluents, and a single form link to inject events into the program. It also has link to kill (lps_terminate) the program.
The fluent display and event injection links can be copied from the page into a browser address bar and reused:
The HTTP status of the events response will be either 200 (OK) or 409 (conflict with the server program integrity constraints).
Both the fluents and events pages display also the LPS cycle time of sampling and injection, respectively.
The events web service above can also respond with fluents, sampled in the cycle prior or after event injection, by simply adding query variables
fluents and (optionally)
The above will return the state of fluent available after the pickup event (and others in the same cycle) are processed.
Open http://lcdemo.logicalcontracts.com/example/diningPhilosophers-table.pl ; launch a LPS server, by executing the proposed goal serve(ID)
Follow the "Manage XXX" link and see the resulting page. Refresh it and see time gone by. Follow the fluents link.
Back to the manager page, edit the "events to send" field to: [pickup(miguel,fork1)], and click Send, and see the "Events result" page. Then refresh it, and see how the second instance of the same event is rejected by preconditions in the server.
Refresh the fluents page; you should see a different state.
At some point you may get a "thread XXX does not exist", meaning that that particular program execution has finished. Go back to http://lcdemo.logicalcontracts.com/example/diningPhilosophers-table.pl and launch another server.
Next we take the dining philosphers example and split it into two: a "table" with domain conditions, and a "client" with the philosophers and their layout and intentions:
Open http://lcdemo.logicalcontracts.com/example/diningPhilosophers-table.pl ; launch a LPS server, by executing the proposed goal serve(ID). Copy the LPS server thread ID (e.g. lps1) obtained from the LPS manager page, or from the end of its URL.
Open http://lcdemo.logicalcontracts.com/example/diningPhilosophers-client.pl; edit the proposed goal to carry the relevant LPS server ID obtained above, e.g. ... + table(lps1)..., and run it. You should see a textual run of dining philosophers.
LPS programs can have their execution suspended: its whole state is saved as a single term, including pending goals; it finishes; and it can be resumed later, given the original program and the saved execution state.
A LPS program can save its state anytime by invoking the system action:
A LPS web server can also be suspended, serving the saved state term in the resulting page. This operation is available from the server manager page. The current URL is of the form:
Notice that the special event and "fluent" used may have acess restrictions.
A LPS program can resume, or start from a previously "hibernated", saved state.
Hibernation requires that the program is still the same, or more precisely, equivalent. A LPS program is deemed equivalent for hibernation purposes if:
Notice that although "LPS simulation time" (cycles) are independent of hibernation, real time isn't. For example, consider a program with a real time execution limit of 1 hour, that is suspended after just 1 minute, with 59 minutes left; it it is resumed a day later, it will start but finish immediately.
The simplest way to resume an execution is to include the saved state in the program source code itself, e.g.
When starting the program the LPS engine checks for a lpssavedstate(...) term in the source. If there is one, it uses to "jumpstart" the program from the cycle when it was saved.
The restore option allows a program to (re)start farther ahead in its computation: if present, the SavedStateFile is used to preset goals, reactive rules, cycle number etc in the engine before executing the program.
If the saved state is not compatible with the program, execution is aborted.
Some operations require the user to be authenticated: lps_send_email, google nlp calls, and likely others in the future. To circumvent this requirement (e.g. for development purposes), uncomment
Other operations are allowed only to a specific (operation-relative) user:
See INSTALL_server.md for more about LPS user authentication predicate
lps_user(User) and necessary system configuration.
Prolog predicates can be called from any LPS clause, implicitly as timeless predicates: their results are assumed repeatable and constant over time, without a relevant impact on the world outside the program.
But sometimes, when their resuls or relevant side-effects are time-dependent, it's convenient to embed them instead as time-dependent literals in LPS, so that their execution can be articulated in time and meaning with the rest of the time-dependent logic. The following LPS extensions allow it:
F at Thas no corresponding fluent declaration, but F is defined as a Prolog predicate, then F is assumed to be an "external extensional fluent".
A from T1 to T2has no corresponding action declaration, but A is defined as a Prolog predicate, then A is assumed to be an "external basic action".
In this way the above time variables will be bound to the LPS cycles when the fluent was sampled (
T) and the action executed (
Notes about the Prolog predicate:
Sometimes it's useful to poll some state (or call some builtin function) in the "outside world". So declaring...
prolog_events P, Q, ... .
... will "inject" these events if the corresponding Prolog goals succeed. Notice that a Prolog predicate with the name and arity of P must exist and be accessible in the user module.
events random(X). fluents dice(_Turn,_Face). random(X) from _ to T2 initiates dice(T2,Face) if Face is round(X*6+0.5).
random/1, a Prolog system predicate, gets called at each cycle, initiating dice/2 fluent tuples over time.
The above could in principle be achieved instead with the following pseudo code for each event:
observe([P],T) :- current_time(T), findall(P,P,Ps), member(P,Ps).
... or also with the following LPS pseudo-code:
events P actions P. fluents polling. initially polling. if polling then callprolog(P), P.
Again, the Prolog generated events are injected/checked/etc with observations and web events at each LPS cycle.
For convenience the following action verbs are available, to directly "edit" the designated fluents without the need to resort to an additional action definition:
update Old to New in fluent(..,Old,..)
Time arguments (from.., to..) are implicit.
To understand their meaning, consider the following example not using the above:
fluents gameOn. actions finishGame. finishGame terminates gameOn. % in some reactive rule: ...., finishGame from _ to _,...
Instead one can simply write:
fluents gameOn. % in some reactive rule: ....,terminate gameOn from _ to _,...
The system has an explanation facility, capable of justifying any contract fluent value or action occurrence in time; the explanation is the set of rule instances necessary for the result.
The current preliminary implementation is still textual and non optimized, but can be tried on any program with:
For an example open up this example and try in the query panel:
There is also an explanation for why something did NOT occur; these explanations are in general much bigger:
Again, these are still preliminary, do NOT yet depend on them for production work.
The LC Server includes an Ethereum node with wallet, which contracts can use. The following system predicates can be tried at http://demo.logicalcontracts.com/ ; you may be asked to login with a Google account.
All of these can be used as fluents or actions.
The following system predicate gives access to the full Ethereum API as defined in https://github.com/ethereum/wiki/wiki/JSON-RPC:
In addition to each RPC method's arguments, an extra predicate argument with the result should be added. For example the following goal obtains the current balance of the Ethereum node's mining account in Wei:
e( coinbase(A) ), e( getBalance(A,latest,Bhex)), atom_to_term(Bhex,Balance,_).
Notice that the "eth" prefix is not necessary - but others such as net are. The e(...) predicate results are in "raw" hexadecimal. The following functions can be used for conversions:
To avoid these explicit conversions, there's a higher-level API.
V is returned as the current balance (in Wei) of account A; Block can be a number, 'latest' or other constant.
Send a transaction, optionally with a data value
This checks whether a receipt exists in the latest block for the transaction.
The following is to obtain accounts (loaded with a little Ether) for experimentation in our demo server:
NOTE: In the demo server transactions can NOT be sent to external (non local) accounts by unauthorized users. Contact firstname.lastname@example.org if your project requires it.
A program may contain a en("...") fact with a Formal English specification for LPS rules, thereby becoming executable. For an elaborate example see http://demo.logicalcontracts.com/example/RockPaperScissorsBase.pl
dumplps to print the resulting LPS program on the console, in surface syntax (or
dump to get the internal syntax).
Any LPS program can be displayed in Formal english by using