Logical Contracts Server

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

real_time(RT) at T

System fluent that returns the real time (seconds since Jan 1, 1970) at the begin of LPS cycle T.

real_time_beginning(RTB)

Timeless predicate that returns the (real) time when the LPS execution began.

maxRealTime(Seconds)

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.

Background execution

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).

background(ID) option

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.

minCycleTime(Seconds)

Add a fixed "sleep" time to the program execution at the begin of each cycle, for the sake of the server environment.

interpreter:inject_events(+LPSengineThread,+Events,-Result)

Inject all events into the LPS server thread, after inserting whatever observations are declared for the program. See interpreter:updateEvents/3.

If successful, Result = ok(InsertionCycle); else, e.g. if some event violates the program integrity constraints, all events are rejected and `Result = failed(Cause)

interpreter: get_fluents(+LPSThreadID,+Fluents,-Cycle,-Values)

Fetches current values for all templates in Fluents into Values. Returns also the Cycle at which the values were samples. See answerthreadqueries/1.

Experimental LPS inter-program calling

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).

LPS web servers

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).

Prolog predicates

For use in the SWISH goal field.

serve(-ID)

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.

servers(IDs)

Shows links to managers for all running LPS programs of the current user.

servers

Shows all LPS program threads IDs, even after they're finished.

kill_all_servers

Brutal cleanup, kills LPS programs of all users.

Servers UI

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:

http://lcdemo.logicalcontracts.com/lps_server/fluents/ProgramID?fluents=[FluentTemplates]

http://lcdemo.logicalcontracts.com/lps_server/events/ProgramID?events=[EventAtoms]

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) after:

http://lcdemo.logicalcontracts.com/lps_server/events/ProgramID?events=[pickup(kant,fork1)]&fluents=[available(_)]&after=true

The above will return the state of fluent available after the pickup event (and others in the same cycle) are processed.

Example

Basics

• 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.

Philosophers dining remotely

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.

Hibernation

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.

Saving execution state

A LPS program can save its state anytime by invoking the system action:

lps_save_finish_execution(File)

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:

/lps_server/events/ID?events=[lps_terminate]&fluents=[lps_saved_state(_,_,_,_,_,_)]&after=true

Notice that the special event and "fluent" used may have acess restrictions.

Resuming a saved execution

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:

• Its internal syntax form, serialised as in the source program, is the same (modulo term variants). This is ensured by computing a SHA256 hash of the text, excluding program comments and white space.
• The engines used for saving and restoring are version compatible.

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.

Bundling a saved state in the program

The simplest way to resume an execution is to include the saved state in the program source code itself, e.g.

lps_saved_state('0872e13090f71236da7ffb7dabd62e5a',t(1505983225.885826,454,date(2017,9,21,8,40,31.391840934,0,'UTC',-)),[],[],[available(fork1),available(fork2),available(fork3),available(fork4),available(fork5),real_time(1505983231.391349)],[]).

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(File) option

golps(ProgramFile,[...restore(SavedStateFile)..])

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.

Authentication and permissions

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 allow_anonymous_powerful_ops.

Other operations are allowed only to a specific (operation-relative) user:

• lps_terminate events are allowed into a LPS server only if the client has the same user that created the server
• LPS server manager pages are accessible only to the user that created the server

See INSTALL_server.md for more about LPS user authentication predicate lps_user(User) and necessary system configuration.

External (Prolog) fluents and actions

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:

• If a literal F at T has no corresponding fluent declaration, but F is defined as a Prolog predicate, then F is assumed to be an "external extensional fluent".
• If a literal A from T1 to T2 has 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 (T1,T2).

Notes about the Prolog predicate:

• It can be defined together with the LPS program, or elsewhere in the Prolog system.
• It is always called via findall, as the LPS engine will use its different answer bindings to pursue parallel goals. Predicate failure makes the action incompatible, as if violating a precondition.
• External fluents can NOT be the fluent in a post condition (although it can be referred in its condition).

External (Prolog) events

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.

Example:

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.

Other misc LPS engine improvements

• Generic replace/update post conditions, e.g. transfer(From, To, Amount) updates Old to New in balance(From, Old) if New is Old – Amount. Old/New can be (structurally similar) lists of variables.
• More flexible preconditions/constraints, referring both the current and the next states. For example, the goat cannot be left alone with the cabbage and the goat cannot be left alone with the wolf.
• Aggregate predicate: findall(X,FluentGoal,L) at T.
• Negated fluent conditions.
• Multiple actions in the same cycle are serialized wrt state change, thereby enabling accumulation/aggregation of fluent changes, unless declared unserializable.
• Macro actions starting at the same time are parallelized

A logical explanation

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.

Editing Actions

For convenience the following action verbs are available, to directly "edit" the designated fluents without the need to resort to an additional action definition:

• initiate Fluent
• terminate Fluent
• 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 _,...

Explanations

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:

why(holds(Fluent,Time)).

why(happens(Action,T1,T2)).

For an example open up this example and try in the query panel:

why(happens(pay(bob,2000),2,3)).

There is also an explanation for why something did NOT occur; these explanations are in general much bigger:

whynot(holds(Fluent,Time)).

whynot(happens(Action,T1,T2)).

Again, these are still preliminary, do NOT yet depend on them for production work.

Ethereum blockchain interface

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.

Low-Level API

The following system predicate gives access to the full Ethereum API as defined in https://github.com/ethereum/wiki/wiki/JSON-RPC: e( method(Argument1,Argument2,..Result)

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:

atom_to_term(Hexadecimal,Number,_).
ethereum:hex_to_string(Hexadecimal,String).

To avoid these explicit conversions, there's a higher-level API.

High-level API

e_getBalance(A,Block,V) V is returned as the current balance (in Wei) of account A; Block can be a number, 'latest' or other constant.

e_sendTransaction(From,To,Value,Tx), e_sendTransactionWithAtom(From,To,Value,Atom,Tx) Send a transaction, optionally with a data value Atom.

e_existsTransactionReceipt(Tx) 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:

grab_test_accounts(N,MinEth,Accounts)

NOTE: In the demo server transactions can NOT be sent to external (non local) accounts by unauthorized users. Contact support@logicalcontracts.com if your project requires it.

Formal English

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

Use 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 dumpen.