#lang scribble/manual

@(require scribble/example racket/sandbox
	  (for-label "../dynamics.rkt" typed/racket/base
	  	     (only-in racket/class object%)))

@(define-syntax-rule (deftypeform . args)
  (defform #:kind "type" . args))

@(define-syntax-rule (deftype . args)
  (defidform #:kind "polymorphic type" . args))

@title[#:tag "dynamics"]{dds/dynamics: Dynamics of DDS}

@defmodule[dds/dynamics]

This module provides a number of general definitions for building and analyzing
the dynamics of discrete dynamical systems.

@defclass[dds% object% ()]{

The abstract base class for discrete dynamical systems.

This class has two type parameters:

@itemize[

@item{@racket[State] --- a state of the discrete dynamical system,}

@item{@racket[Modality] --- a description of the way in which the discrete
dynamical system transitions from a given state @italic{s} to another state
@italic{s}.  For systems whose states are described by a set of variables,
a @racket[Modality] is typically a list of variables updated during the
state transition.}

]

@defmethod[(step [st State]) (Listof State)]{

Given a state @racket[st], produces the next states of the state.

This method falls back to calling @method[dds% step/annotated], and then
discarding the annotations.

}

@defmethod[(step/annotated [st State]) (Listof (Pairof Modality State))]{

Given a state, produces the next states paired with the corresponding
modalities. Typical usage would include giving the information about the
update mode.

This method has no fallback and must be overridden.

}

@defmethod[(step* [sts (Listof State)]) (Listof State)]{

Given a set of starting states, produce the set of states reachable in
one step.

This method falls back to running @method[dds% step] for all states.

Note that @method[dds% step*] has no direct @tt{/annotated} counterpart.
This is because producing a list of @racket[(Pairof Modality State)] would not
give enough information to identify to which particular transition the modality
corresponds to.

}

@defmethod[(build-state-graph [sts (Listof State)]) Graph]{

Given a set of starting states, produces the state graph reachable from the
starting states.

This method falls back to exploring the state graph with @method[dds% step].

}

@defmethod[(build-state-graph/annotated [sts (Listof State)]) Graph]{

Given a set of starting states, produces the labelled state graph reachable
from the starting states.

This method falls back to exploring the state graph with @method[dds%
step/annotated].

}

@defmethod[(build-state-graph* [sts (Listof State)] [nsteps Integer]) Graph]{

Given a set of starting states and a number @racket[nsteps] of steps to run,
produces the state graph reachable from the starting states @racket[nsteps] steps.

This method falls back to exploring the state graph with @method[dds% step].

}

@defmethod[(build-state-graph*/annotated [sts (Listof State)] [nsteps Integer])
					 Graph]{

Given a set of starting states and a number @racket[nsteps] of steps to run,
produces the labelled state graph reachable from the starting states
@racket[nsteps] steps.

This method falls back to exploring the state graph with @method[dds%
step/annotated].

}

}