AbacusSim


Automata

This module implements functions for working with automata, in particular,
determinizing them by RabinScott and the Breakpoint construction, as well
as converting omegaautomata to other acceptance conditions.

BooleanFunctions

This module implements functions for generating some special boolean
functions like arithmetic circuits for addition, subtraction, multiplication,
threshold functions, the hidden weighted bit functions, the queen's problem,
and the pigeonhole problems.

CacheCoherence


CircuitGenerators

This file implements functions for generating computer arithmetic ciruits.
The overall idea is that the circuit is generated as a side effect when
calling a generator function with input bitvectors. The generator function
is thereby given the input and output bitvectors as string[]. This way,
also circuits for arithmetic expressions can be generated.

ComputerArithmetic

This file implements functions for radix integer arithmetic

DataflowDesynchronization

This module implements data types and functions to reason about dataflow
process networks. Among others, there are functions to classify a node
concerning sequentiality, (weak) endochrony, Kahn criteria and to run
a network of nodes on a given input state.

DataflowStaticScheduling

This module implements algorithms for analyzing dataflow process networks.
In particular, for static DPNs it can decide whether there is a static
periodic schedule and whether the DPN is bounded, and for dynamic DPNs,
it can compute the product firing table for the entire DPN and can decide
about the (weak) endochrony and Kahn criteria of its nodes.

Encodings


Global

This module implements global functions and constants for the teaching tools.

Grammars

This module

InterconnectNetworks

This file implements algorithms about interconnection and sorting networks
used in computer systems. In particular, there are functions to determine
the configurations of Beneš and Banyan networks with 2way switches.
Since routing is a special case of sorting (where only permutations are
considered), we also consider sorting networks as interconnection networks.
In particular, Batcher's Bitonic and OddEven divide/sort/merge based
networks are considered, with the isomorphic version of Parberry's pairwise
sorting network, and also Dowd's periodic balanced network that allows the
reuse of the periodic block. For all of these configurations, there are
functions to write the resulting network in form of SVG images.
There is also a function to verify whether a given comparator network is a
sorting network, and also a function to determine a

InterconnectNetworksBySMV

This file implements functions to generate SMV files for synthesizing
correct sorting/splitter networks for a given number of inputs and a
desired depth. Further options are found by the global variables below.

KripkeStructures

This module implements functions for checking (bi)simulation relations of
labeled transition systems (Kripke structures). It also computes quotients
and products of Kripke structures.

Mastermind

This module contains functions around the Mastermind board game like some
wellknown strategies like the MinMax, Entropy, ExpectedSize and MaxParts
strategies.
Mastermind is a simple twoplayer codebreaking board game invented in 1970
by Mordecai Meirowitz, an Israeli postmaster and telecommunications expert.
It may have been inspired by moo, a program developed by J.M. Grochow at MIT
in the late 1960s.
In the game, one player is the codemaker and the other is the codebreaker.
The codemaker secretly selects a code consisting of an ordered sequence of
four colors (c_1,c_2,c_3,c_4), each chosen from a set of six possible colors,
with repetitions allowed. The codebreaker then tries to guess the code by
repeatedly proposing a sequence of colors (g_1,g_2,g_3,g_4). After each
guess, the codemaker tells the codebreaker two numbers (b,w): the number of
correct colors in the correct positions (p) and the number of colors that
are part of the code but not in the correct positions (w). For example, if
the code is (1,2,3,3) and the codebreaker's guess is (3,2,4,3), then the
codemaker's response would be (2,1), since the codebreaker has guessed the
2 and the second 3 correctly and in the correct positions, while having
guessed the first 3 correctly but in the wrong position.
The codebreaker continues guessing until she guesses the code correctly or
until she reaches a maximum allowable number of guesses without having
correctly identified the secret code.
Note that w can be computed as w=(sum_(i=1)^numColors min(c_i,g_i))b,
where c_i is the number of times the color i is in the code and g_i is the
number of times it is in the guess.

MiniC

This module implements functions for compiling MiniC to cmd programs,
performing dataflow analysis, displaying CFGs, and generating code for
Abacus.

ModelCheckingExplicit

This module implements functions for global and local model checking of
mucalculus and CTL formulas of explicitly defined Kripke structures. It
also provides functions for some Kripke structure examples like the NIM
game.

ModelCheckingInduction

This module implements functions for verification of safety properties
using induction; in particular functions for incremental induction as
used in property directed reachability (PDR). In contrast to reals PDR
implementation that are based on SAT solvers (and clause sets), this
version is based on BDDs.

ModelCheckingSymbolic

This module implements functions symbolic model checking of mucalculus
and temporal logics. The model checking algorithms are mainly implemented
by means of BDDs. There is also a function for symbolic computation of
predecessor and successor states using quantifier elimination.

Parser

This module implements functions for parsing propositional logic and
temporal logic formulas by simplifying the functions provided in Averest.

PartialOrders

This module implements functions for checking whether a given binary
relation satisfies some properties of partial orders, directed sets, and
lattices. It is restricted, however, to finite relations and sets.

PropLogic

This module implements functions for dealing with propositional logic like
computing truth tables, evaluating formulas by truth assignments, computing
canonical CNF and DNF and the sequent calculus.

Quartz

This module first implements functions and data types for generating an
extended finite state machine for a given Quartz program (without module
calls). Furthermore, functions to generate verification conditions are
provided which are based on induction on the EFSM states and strongly
connected components.

RandomGenerator

This module implements

ReactiveSynthesis

This module implements functions for solving parity games with Zielonka's
algorithm.

ScadBasicBlocks

This module implements functions for scheduling the code of a basic block
to a SCAD machine with a given number of universal processing units. Note
that the problem is NPcomplete!

SurveyQuestion


WeakMemory

