Third-Party Software

As most free software, ALASKA relies on third-party components. To avoid painful compilation steps, these components are included pre-compiled in the downloadable archive. In no way would I like to overshadow the time and effort put into the development of these components or claim that they are my own, so here's the list of packages that ALASKA is bundled with :

• CUDD 2.4.1, by Fabio Somenzi
• PyCUDD 2.0.1, by Steve Haynal and Aravind Vijayakumar
• PLY : Python Lex Yacc, by David M. Beazley
• A customized version of NuSMV 2.4.3, by a (large) number of people. For those interested in the patch, it is included in the ALASKA archive.

Installation Instructions

Requirements

ALASKA runs on Linux, Mac (both PPC and Intel), and Windows systems using Cygwin.
In all cases, the only dependency is Python 2.5.

Step-by-step guide

You can download ALASKA here.
As of version 0.4, Alaska works out of the box without any compilation hassles, enjoy !
Simply decompress the archive and run the file alaska-0.4/bin/alaska
For additional comfort, you can add the directory alaska-0.4/bin to the PATH environment variable.

Commandline interface

The "alaska" script in the bin/ directory is the main executable of ALASKA.
Simply run the script without any arguments and you will get the list of available options.

Input Syntax for LTL and Alternating Automata

LTL Formulas

The syntax form LTL formulas is the union of those of Spin and NuSMV.

• Promela LTL Syntax
• NuSMV LTL Syntax

Note that only "future" operators are supported.

Alternating Automata

The input syntax for alternating automata is really simple, here is an example :

  (
    automaton_type = "sABW",
    locations = [0,1,2,3,4],
    propositions = ["p0","p1"],
    initial_constraint = "0",
    transition_function =   {
       0 : "(p0 & 1) | (~p1 & 1 & 2)"
     , 1 : "p1 & 1 & 3"
     , 2 : "true"
     , 3 : "4 | ~p0"
     , 4 : "false"
    },
    accepting_locations = [1,4]
  )

To facilitate the illustration of the syntax, here's a graphical representation of this automaton :

As you may have noticed, the input file for alternating automata is actually a Python mini-script.
The first thing to remember is thus to respect the Python syntax.
For those who know a bit of Python : Alaska evaluates dict(%s) where %s is the input string withouth leading/trailing parentheses.
The script needs to assign the following variables :

• automaton_type : either 'sAFW' or 'sABW'
• locations : a list of contiguous integers starting at 0. You may use the range() function here.
• propositions : a list of strings representing the atomic propositions.
• initial_constraint : a string representing the Boolean formula of the initial constraint.
• transition_function : the transition function
• accepting_locations : the list of accepting nodes

Note that the accepting_locations are either interpreted as a Buechi condition
or a finite accepting set, depending on automaton_type.

The transition_function variable must be a dictionnary that maps each location
to a Boolean formula over the propositions and locations.
Note that locations can only be constrained positively !

The following syntax can be used in boolean formulas :

• () : parentheses can be used freely
• | : is the "OR" boolean operator
• & : is the "AND" boolean operator
• ~ or !: is the "NOT" boolean operator
• true : is the "true" constant
• false : is the "false" constant