2022-07-06 00:00:17 +02:00
|
|
|
#lang scribble/manual
|
|
|
|
|
|
|
|
@(require scribble/example racket/sandbox
|
2022-08-23 10:17:58 +02:00
|
|
|
(for-label "../dynamics.rkt" typed/racket/base
|
|
|
|
(only-in racket/class object%)))
|
2022-07-06 00:00:17 +02:00
|
|
|
|
|
|
|
@(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.
|
|
|
|
|
2022-08-23 10:17:58 +02:00
|
|
|
@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].
|
|
|
|
|
|
|
|
}
|
|
|
|
|
2022-09-15 01:11:11 +02:00
|
|
|
@defmethod[(build-state-graph* [sts (Listof State)]
|
|
|
|
[nsteps (U Positive-Integer 'full)])
|
|
|
|
Graph]{
|
2022-08-23 10:17:58 +02:00
|
|
|
|
|
|
|
Given a set of starting states and a number @racket[nsteps] of steps to run,
|
2022-09-10 18:55:03 +02:00
|
|
|
produces the state graph reachable from the starting states @racket[nsteps]
|
|
|
|
steps. If @racket[nsteps] is @racket['full], constructs the full state
|
|
|
|
graph instead.
|
2022-08-23 10:17:58 +02:00
|
|
|
|
|
|
|
This method falls back to exploring the state graph with @method[dds% step].
|
|
|
|
|
|
|
|
}
|
|
|
|
|
2022-09-15 01:11:11 +02:00
|
|
|
@defmethod[(build-state-graph*/annotated [sts (Listof State)]
|
|
|
|
[nsteps (U Positive-Integer 'full)])
|
2022-08-23 10:17:58 +02:00
|
|
|
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
|
2022-09-10 18:55:03 +02:00
|
|
|
@racket[nsteps] steps. If @racket[nsteps] is @racket['full], constructs the
|
|
|
|
full state graph instead.
|
2022-08-23 10:17:58 +02:00
|
|
|
|
|
|
|
This method falls back to exploring the state graph with @method[dds%
|
|
|
|
step/annotated].
|
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
}
|