alice
library
manual.

Alice Project

The Space structure


________ Synopsis ____________________________________________________

    signature SPACE
    structure Space : SPACE

The Space structure provides access to first class computation spaces. First class computation spaces can be used to program inference engines for problem solving.

For example, simple depth-first one solution search can be done as follows.

    fun searchOne s =
	case ask s of
	     FAILED          => NONE
	   | SUCCEEDED       => SOME (Space.merge s)
	   | ALTERNATIVES(n) =>
		 let
		     val c = Space.clone s
		 in
		     Space.commit(s, SINGLE 1);
		     case searchOne s of
			  NONE   => (Space.commit(c, RANGE(2, n)); searchOne c)
			| SOME s => SOME s
		 end

Given the money script, a solution can be searched by invoking

    val solution = searchOne (Space.space money)

More sophisticated search engines are provided by the structure Search.


________ Import ______________________________________________________

    import signature SPACE from "x-alice:/lib/constraints/SPACE-sig"
    import structure Space from "x-alice:/lib/constraints/Space"

________ Interface ___________________________________________________

    signature SPACE =
    sig
	eqtype 'a space
	    
	datatype state =
	    MERGED
	  | FAILED
	  | SUCCEEDED
	  | ALTERNATIVES of int

	datatype verbose_state =
            VERBOSE_SUSPENDED of verbose_state
	  | VERBOSE_MERGED
	  | VERBOSE_FAILED
	  | VERBOSE_SUCCEEDED_STUCK
	  | VERBOSE_SUCCEEDED_ENTAILED
	  | VERBOSE_ALTERNATIVES of int
	    
	datatype choice =
	    SINGLE of int
	  | RANGE of int * int
	    
	val space : (unit -> 'a) -> 'a space
	    
	val ask : 'a space -> state
        val askVerbose : 'a space -> verbose_state
	val clone : 'a space -> 'a space
	val commit : 'a space * choice -> unit
	val inject : 'a space * ('a -> unit) -> unit
	val merge : 'a space -> 'a
        val kill : 'a space -> unit
        val waitStable : 'a space -> unit
    end

________ Description _________________________________________________

eqtype 'a space

The type of computation spaces.

datatype state = MERGED | FAILED | SUCCEEDED | ALTERNATIVES of int

This datatype is used to communicate the state of a computation space.

datatype verbose_state = VERBOSE_SUSPENDED of verbose_state | VERBOSE_MERGED | VERBOSE_FAILED | VERBOSE_SUCCEEDED_STUCK | VERBOSE_SUCCEEDED_ENTAILED | VERBOSE_ALTERNATIVES of int

This datatype is used to communicate the verbose state of a computation space.

datatype choice = SINGLE of int | RANGE of int * int

This datatype is used to select alternatives of the selected choice of a space.

space p

returns a newly created space, in which a thread containing an application of the unary function p to the root variable of the space is created.

ask s

waits until s becomes stable or merged and then returns the state of s.

If s is merged, MERGED is returned.

If s is stable and failed, FAILED is returned.

If s is stable and succeeded and there are no threads in s synchronizing on choices, SUCCEEDED is returned.

If s is stable and succeeded and there is at least one thread in s which synchronizes on a choice, ALTERNATIVES i is returned, where i gives the number of alternatives on the selected choice.

Synchronizes on stability of s.

Raises a runtime error if the current space is not admissible for s.

askVerbose s

returns the state of s in verbose form. Reduces immediately, even if s is not yet stable.

If s becomes merged, VERBOSE_MERGED is returned.

If s becomes suspended (that is, blocked but not stable), VERBOSE_SUSPENDED t is returned. t is a future that is bound to the verbose state of s when s becomes stable again.

If s is stable and failed, VERBOSE_FAILED is returned.

If s is stable and succeeded and there are no threads in s synchronizing on choices, either VERBOSE_SUCCEEDED_STUCK, or VERBOSE_SUCCEEDED_ENTAILED is returned. The former happens when s still contains threads.

If s is stable and succeeded and there is at least one thread in s which synchronizes on a choice, VERBOSE_ALTERNATIVES i is returned, where i gives the number of alternatives on the selected choice.

Does not synchronize on stability of s.

Raises a runtime error if the current space is not admissible for s.

clone s

blocks until s becomes stable and returns a new space which is a copy of s.

Synchronizes on stability of s.

Raises a runtime error if s is already merged, or if the current space is not admissible for s.

commit (s, c)

blocks until s becomes stable and then commits to alternatives of the selected choice of s.

if c is RANGE(l, h), then all but the l,l+1,...,h alternatives of the selected choice of s are discarded. If a single alternative remains, the topmost choice is replaced by this alternative. If no alternative remains, the space is failed.

SINGLE i is an abbreviation for RANGE(i, i).

Synchronizes on stability of s.

Raises a runtime error, if s has been merged already, if there exists no selected choice in s, or if the current space is not admissible for s.

inject (s, p)

creates a thread in s which contains an application of p to the root variable of s.

Does not synchronize on stability of s.

Raises a runtime error if s is already merged, or if the current space is not admissible for s.

merge s

merges s with the current space and returns the root variable of s.

Does not synchronizes on stability of s.

Raises a runtime error if s is already merged, or if the current space is not admissible for s.

kill s

kills s by injecting a failure into a space.

waitStable s

Synchronizes on stability of s and returns unit.



last modified 1970/01/01 01:00