lomap 0.1.1.post1

LTL Optimal Multi-Agent Planner (LOMAP)

LTL Optimal Multi-Agent Planner (LOMAP)
Copyright (C) 2012-2015, Alphan Ulusoy ([e-mail])

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301, USA.

A copy of the GNU General Public License is included in this
distribution, in a file called 'COPYING'.

----------------------------------------------------------------------

LTL Optimal Multi-Agent Planner (LOMAP) is a python package for
automatic planning of optimal paths for multi-agent systems.
See the directory 'examples' (either in the source archive or in
the installation directory) for examples.

----------------------------------------------------------------------

LOMAP uses two third party programs: LTL2BA and scheck. You can
find their sources in this distribution, in a directory called
'third_party_sources'. For your convenience, binaries of these
programs are already included in this distribution, in a folder
called 'binaries'. LOMAP also includes some code that is adapted
and/or taken from NetworkX Python package v1.6, available at
http://networkx.github.io. See below for copyright notices and
licenses of LTL2BA, scheck, and NetworkX.

LTL2BA
------
LTL2BA - Version 1.0 - October 2001
Written by Denis Oddoux, LIAFA, France
Copyright (C) 2001 Denis Oddoux

LTL2BA - Version 1.1 - August 2007
Modified by Paul Gastin, LSV, France
Copyright (C) 2007 Paul Gastin
Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version. GNU GPL is included in this
distribution, in a file called 'LICENSE'

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

The LTL2BA software was written by Denis Oddoux and modified by Paul
Gastin. It is based on the translation algorithm presented at CAV '01:
P.Gastin and D.Oddoux
"Fast LTL to Büchi Automata Translation"
in 13th International Conference on Computer Aided Verification, CAV 2001,
G. Berry, H. Comon, A. Finkel (Eds.)
Paris, France, July 18-22, 2001,
Proceedings - LNCS 2102, pp. 53-65

Send bug-reports and/or questions to Paul Gastin
http://www.lsv.ens-cachan.fr/~gastin

Part of the code included is issued from the SPIN software Version 3.4.1
The SPIN software is written by Gerard J. Holzmann, originally as part
of ``Design and Validation of Protocols,'' ISBN 0-13-539925-4,
1991, Prentice Hall, Englewood Cliffs, NJ, 07632
Here are the files that contain some code from Spin v3.4.1 :

cache.c (originally tl_cache.c)
lex.c ( tl_lex.c )
ltl2ba.h ( tl.h )
main.c ( tl_main.c )
mem.c ( tl_mem.c )
parse.c ( tl_parse.c)
rewrt.c ( tl_rewrt.c)
trans.c ( tl_trans.c)

scheck
------
scheck - Version 1.2
Copyright (C) 2003 Timo Latvala ([e-mail])
Modified by Amit Bhatia, Computer Science Department, Rice University
Copyright (C) 2011 Amit Bhatia

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

scheck is a tool for translating safety LTL formulae to finite automata.
The algorithm used in the tool was presented in the paper:

Timo Latvala. Efficient Model Checking of Safety Properties. In:
T. Ball and S.K. Rajamani (eds.), Model Checking Software. 10th
International SPIN Workshop. Volume 2648 of LNCS, pp. 74-88, Springer, 2003.

This version of scheck incorporates some changes into scheck 1.2 that
is available for download from Timo Latvala's website. The changes were
made so that scheck could be compiled on newer gcc compilers. The code
compiles fine with gcc 4.4.5. However, please note that I am not the
original developer or the current maintainer of this code. For further
details, please refer to README.html.

Amit Bhatia, Computer Science Department, Rice University,
April 7, 2011.

NetworkX
--------
Copyright (C) 2004-2012, NetworkX Developers
Aric Hagberg <[e-mail]>
Dan Schult <[e-mail]>
Pieter Swart <[e-mail]>
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.

* Neither the name of the NetworkX Developers nor the names of its
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.


THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.