Machines

Module tock.machines

This module contains Tock’s main data structure, the Machine class, and associated classes and functions.

class tock.machines.Machine(store_types, state=None, input=None)

A machine (automaton) that accepts or rejects strings. It has one or more stores, which can act as states, stacks, tapes, etc. When it is run on a string, the stores are initialized to a start configuration and rewritten by transitions until an accept configuration is reached or no more rewrites are possible.

Parameters:

  • store_types – A list of store types, one for each store. Allowed types are BASE, STREAM, and TAPE. See add_transition and add_accept_state for explanation of these types.

  • state (int) – The index of the store which is the state. The state is usually what distinguishes the start and accept configurations, and it is also treated specially when reading/writing machines.

  • input (int) – The index of the store which is the input store. When the machine is run on a string, the input store is initialized to the string.

High-level interface

property num_stores

How many stores the Machine has.

add_transition(transition)
add_transition(lhs, rhs)

Add a transition. The argument can either be a Transition or a left-hand side and a right-hand side.

  • If a store is a STREAM, there should not be an rhs; an empty rhs is automatically inserted.

  • If a store is a TAPE, there should be two rhs’s: a write (whose position is ignored) and a move (L or R).

add_transitions(transitions)

Add a list of transitions (see add_transition).

get_transitions()

Return an iterator over all transitions, as AlignedTransitions.

  • For any stores of type STREAM, the generated transitions do not have an rhs for the input.

  • For any stores of type TAPE, the generated transitions will have an additional field to indicate a move (L or R).

property states

The set of all possible states.

set_start_state(q)

Set the start configuration with q as the start state. The input store will be initialized to the input string, and all other stores will be initialized to the empty string.

get_start_state()

Return the start state.

add_accept_state(q)

Add an accept configuration with q as the state. Any stores with type STREAM must reach the end of the string in order to accept. All other stores will not have any accepting conditions.

add_accept_states(qs)

Add a list of accept states (see add_accept_state).

get_accept_states()

Return the set of accept states.

Low-level interface

Tests for different types of automata

is_finite()

Tests whether machine is a finite automaton.

is_pushdown()

Tests whether machine is a pushdown automaton.

is_turing()

Tests whether machine is a Turing machine.

is_deterministic(verbose=False)

Tests whether machine is deterministic.

class tock.machines.Store(values=(), position=0)
class tock.machines.Store(store)

A string together with a head position. It is used either as a store of a Machine or as a pattern to be matched against a store of a Machine.

Parameters:

  • values – Sequence of Symbols

  • position (int) – The head position, between -1 and len(values)

  • store (Store or str) – Another Store to copy, or a str to convert to a Store

values

A sequence of Symbols

match(other)

Returns true iff self (as a pattern) matches other (as a store). Note that this is asymmetric: other is allowed to have symbols that aren’t found in self.

class tock.machines.Configuration(stores)
class tock.machines.Configuration(config)

A configuration, which is essentially a tuple of Stores.

Parameters:

  • stores – A tuple of Stores

  • config (Configuration or str) – Another Configuration to copy, or a str to convert to a Configuration

match(other)

Returns true iff self (as a pattern) matches other (as a configuration). Note that this is asymmetric: other is allowed to have symbols that aren’t found in self.

class tock.machines.Transition(lhs, rhs)
class tock.machines.Transition(transition)

A transition from one Configuration to another Configuration.

Parameters:
match(config)

Returns True iff self can be applied to config.

apply(config)
class tock.machines.AlignedTransition(transitions)

A Transition that has an alignment between the lhs and rhs. These are generated by get_transitions so that even if the number of lhs and rhs stores changes, we can still keep track of their relationship to the machine’s stores.

If t is an AlignedTransition, t[i] is a Transition containing the lhs and rhs just for store number i.

Module tock.operations

This module contains various operations on automata.

tock.operations.determinize(m)

Determinizes a finite automaton.

tock.operations.equivalent(m1, m2)

Test whether two DFAs are equivalent, using the Hopcroft-Karp algorithm.

tock.operations.intersect(m1, m2)

Intersect two Machines.

Both machines should have a state as store 0 and input STREAM as store 1. For example,

  • Both can be finite automata, in which case this is the standard product construction.

  • One can be an NFA and the other a PDA, in which case the result is a PDA.

  • The intersection of two PDAs would be a two-stack PDA.

tock.operations.prefix(m)

Given a NFA m, construct a new NFA that accepts all prefixes of strings accepted by m.

Module tock.run

Runs machine m on string w, automatically selecting a search method.

param m:

The machine to run.

type m:

Machine

param w:

The string to run on.

type w:

String

param trace:

Print the steps of the simulation to stdout.

type trace:

bool

param steps:

Maximum number of steps to run the simulation.

type steps:

int

param show_stack:

For PDAs, the maximum depth of the stack to show.

type show_stack:

int

returns:

A Graph whose nodes are the configurations reachable from the start configuration (which has the attribute start=True). It has an accept configuration (attribute accept=True) iff m accepts w.