Import files from release clone of old MoCS repository

.hg_archival.txt

@@ -0,0 +1,5 @@
+repo: 41eccac6fdd052fca3d42e4d6a7ab8aef775f0f8
+node: e85c0b6a03386649fea9c96f250ddd57e4bb38b4
+branch: default
+latesttag: 0.1
+latesttagdistance: 16

.hgignore

@@ -0,0 +1,45 @@
+# *** MOCS-COPYRIGHT-NOTICE-BEGIN ***
+#
+# This copyright notice is auto-generated by ./add-copyright-notice.
+# Additional copyright notices must be added below the last line of this notice.
+#
+# MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): ".hgignore".
+# The content of this file is copyright of Saarland University -
+# Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz <[email protected]>.
+#
+# This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
+#
+# License: three-clause BSD style license.
+# The license text can be found in the file LICENSE.
+#
+# *** MOCS-COPYRIGHT-NOTICE-END ***
+
+syntax: glob
+doc/*.pdf
+doc/*.log
+doc/*.aux
+test/SuffixRolloutStat
+test/RolloutStat
+test/Rollout
+*.a
+*.orig
+*.o
+vardi*.vhdl
+*.dot
+*.ps
+main
+exprtest
+auttest
+*.hi
+haskell-frontend/Main
+haskell-frontend/Main2
+libaaut.a
+haskell-docs**
+haskell-docs/src/**
+formulas/all.data
+libaaut/tags
+test/aut
+test/rollout
+test/ctest
+formulas/xst
+glob:mocs-*.tar.bz2

.hgsigs

@@ -0,0 +1,3 @@
+6e9c9bdde7b44ad586a0073c421bed726bdfc3a8 0 iEYEABECAAYFAknQoIQACgkQLJDCN6UpI1eRgQCgielKdQHKO8v+/Zgb+WvocpRKk+cAoN/zRwSz9g4n2bHvcRayhxmGl6Fl
+6c65569c9d2536062bd157597bf91f3fb004c3ce 0 iEYEABECAAYFAktFoQIACgkQLJDCN6UpI1f74wCggG6gL5PmIMMiJ1myWf1Dt62ZzkAAoLfCDApmKDHeY+z4VwGZri+MJBIP
+fc3fbc520e5e8e7b791ab6e756d3c67a6d6045a0 0 iEYEABECAAYFAkuRA7IACgkQLJDCN6UpI1c9OACeL/NElMUofvlBtHNKhaIyVX9sgXoAoLBd5rkwR7PCt07RWnmqtybLgEfU

.hgtags

@@ -0,0 +1,3 @@
+6e9c9bdde7b44ad586a0073c421bed726bdfc3a8 used for experimental results in rv 2009
+6c65569c9d2536062bd157597bf91f3fb004c3ce ready for relesae
+3cbf52141620d3d929eb346b721739bd71f43c3d 0.1

LICENSE

@@ -0,0 +1,11 @@
+Copyright (c) 2009, Saarland University
+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 Saarland University 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 HOLDER 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.
+

Makefile

@@ -0,0 +1,46 @@
+# *** MOCS-COPYRIGHT-NOTICE-BEGIN ***
+#
+# This copyright notice is auto-generated by ./add-copyright-notice.
+# Additional copyright notices must be added below the last line of this notice.
+#
+# MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): "Makefile".
+# The content of this file is copyright of Saarland University -
+# Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz <[email protected]>.
+#
+# This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
+#
+# License: three-clause BSD style license.
+# The license text can be found in the file LICENSE.
+#
+# *** MOCS-COPYRIGHT-NOTICE-END ***
+
+ROOT=.
+
+include $(ROOT)/Makefile.pre
+
+.PHONY: archive brelease hsdoc all
+
+MODULEDEPS=libaaut c-bindings haskell-bindings test haskell-frontend # cppfrontend
+
+MODULEDEPSTARGET=$(MAKECMDGOALS)
+
+HSSOURCES:=$(wildcard haskell-bindings/*.hs haskell-frontend/*.hs test/*.hs)
+hsdoc: $(HSSOURCES)
+	mkdir -p haskell-docs/src
+	HsColour -print-css > haskell-docs/src/hscolour.css
+	for i in $^ ; do echo haskell-docs/src/`basename $$i .hs`.html; HsColour -css -anchor $$i > haskell-docs/src/`basename $$i .hs`.html ; done
+	haddock --html --title="psl-monitor-synth" --odir=haskell-docs   \
+	        --source-module='src/%M.html' --source-entity='src/%M.html#%N' $^
+
+archive:
+	hg archive -p mocs -t tbz2 mocs.tar.bz2 -X '\.hg[a-z]*' -X 'add-copyright-notice'
+
+brelease: MODULEDEPSTARGET=
+brelease: haskell-frontend
+	mkdir -p mocs
+	cp LICENSE README haskell-frontend/Main mocs
+	mv mocs/Main mocs/MoCS
+	tar czf "mocs-$(VERSION)-$(shell hg id -i).tar.gz" mocs
+	rm -rf mocs
+
+include $(ROOT)/Makefile.post

Makefile.post

@@ -0,0 +1,64 @@
+# *** MOCS-COPYRIGHT-NOTICE-BEGIN ***
+#
+# This copyright notice is auto-generated by ./add-copyright-notice.
+# Additional copyright notices must be added below the last line of this notice.
+#
+# MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): "Makefile.post".
+# The content of this file is copyright of Saarland University -
+# Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz <[email protected]>.
+#
+# This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
+#
+# License: three-clause BSD style license.
+# The license text can be found in the file LICENSE.
+#
+# *** MOCS-COPYRIGHT-NOTICE-END ***
+
+TARGETS=$(CCBINTARGETS) $(CBINTARGETS) $(LIBTARGETS) $(HSTARGETS)
+
+all: $(MODULEDEPS) $(TARGETS) $(HSMODULETARGETS)
+
+ifneq ($(ROOT),.)
+clean:
+	rm -f $(HIS) $(OBJS) $(TARGETS)
+else
+clean: all
+endif
+
+.PHONY: all clean $(MODULEDEPS)
+
+# Rules:
+
+$(MODULEDEPS): % :
+	$(MAKE) -C $(ROOT)/$@ $(MODULEDEPSTARGET)
+
+$(HSTARGETS): % : %.hs force
+	$(GHC) $(HSOPT) $(HSARGS) --make -o $@ $(CINCS) $(HSINCS) $(LIBPATH) $< $(LIBS)
+
+$(HSMODULETARGETS) : % : %.hs
+	$(GHC) $(HSARGS) $(HSOPT) $(CINCS) -c $<
+
+
+$(CBINTARGETS): % : %.o 
+	$(CC) $(COPT) $(CDEBUG) $(CINCS) $(LIBPATH) -o $@ $^ $(LIBS)
+
+$(CCBINTARGETS): % : %.o
+	$(CPP) $(COPT) $(CDEBUG) $(CINCS) $(LIBPATH) -o $@ $^ $(LIBS)
+
+.c.o:
+	$(CC) -c $(COPT) $(CDEBUG) $(CINCS) -o $@ $<
+
+.cc.o:
+	$(CPP) -c $(COPT) $(CDEBUG) $(CINCS) -o $@ $<
+
+%.a: $(OBJS)
+	ar r $@ $^
+
+# Special targets
+force: ;
+
+MoCSVersion.hs:
+	echo -e "module MoCSVersion where\n mocsVersion = \"$(VERSION)\"\n mocsRevision = \"$(REVISION)\"" > MoCSVersion.hs
+
+ .INTERMEDIATE: MoCSVersion.hs
+

Makefile.pre

@@ -0,0 +1,64 @@
+# *** MOCS-COPYRIGHT-NOTICE-BEGIN ***
+#
+# This copyright notice is auto-generated by ./add-copyright-notice.
+# Additional copyright notices must be added below the last line of this notice.
+#
+# MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): "Makefile.pre".
+# The content of this file is copyright of Saarland University -
+# Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz <[email protected]>.
+#
+# This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
+#
+# License: three-clause BSD style license.
+# The license text can be found in the file LICENSE.
+#
+# *** MOCS-COPYRIGHT-NOTICE-END ***
+
+SHELL = /bin/bash
+
+include $(ROOT)/config.make
+
+.SUFFIXES:
+.SUFFIXES: .c .o .a .cc .hh .tcc .hs .vhdl .h
+
+.DEFAULT_GOAL := all
+
+# Tools
+CC:=gcc
+CPP:=g++
+GHC:=ghc
+
+# Generic file lists
+CCSRCS=$(wildcard *.cc)
+HEADER=$(wildcard *.hh) $(wildcard *.h)
+THEADER=$(wildcard *.tcc)
+HSSRCS=$(wildcard *.hs)
+
+OBJS=$(CCSRCS:.cc=.o) $(HSSRCS:.hs=.o)
+HIS=$(HSSRCS:.hs=.hi)
+
+# C-Icludes
+CINCS=-I$(ROOT)/c-bindings -I$(ROOT)/libaaut
+
+# HS-includes
+HSINCS=-i$(ROOT)/haskell-bindings -i$(ROOT)/haskell-frontend
+
+# library pathes
+LIBPATH=-L$(ROOT)/libaaut -L$(ROOT)/c-bindings
+LIBS=-laautc -laaut -lstdc++
+
+# vpathes
+vpath %.hs $(ROOT)/haskell-bindings:$(ROOT)/haskell-frontend:test
+
+vpath %._c.cc $(ROOT)/c-bindings
+vpath %.h $(ROOT)/c-bindings
+vpath %.hh $(ROOT)/libaaut
+vpath %.cc $(ROOT)/libaaut:$(ROOT)/test
+vpath %.c $(ROOT)/test
+
+vpath libaaut.a $(ROOT)/libaaut
+vpath libaautc.a $(ROOT)/c-bindings
+
+vpath %.vhdl $(ROOT)/vhdl
+
+vpath %.hs $(ROOT)/haskell-bindings:$(ROOT)/haskell-frontend:$(ROOT)/test

README

@@ -0,0 +1,88 @@
+*** MOCS-COPYRIGHT-NOTICE-BEGIN ***
+
+This copyright notice is auto-generated by ./add-copyright-notice.
+Additional copyright notices must be added below the last line of this notice.
+
+MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): "README".
+The content of this file is copyright of Saarland University -
+Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz <[email protected]>.
+
+This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
+
+License: three-clause BSD style license.
+The license text can be found in the file LICENSE.
+
+*** MOCS-COPYRIGHT-NOTICE-END ***
+
+== OVERVIEW ==
+
+MoCS -- Monitor Circuits Synthesis for PSL specifications
+
+MoCS synthesies monitor circuits from linear time temporal logic
+specifications. The input logic is similar to PSL by allowing nesting of
+regular expressions within temporal modalities. The output of MoCS is a
+synthesizable VHDL description of the monitor circuit. The resulting monitors
+implement truncated path semantics. On sequentially reading an input trace a
+monitor outputs at each input position whether the current prefix of the trace
+satisfies the monitored property. MoCS is particularly careful about generating
+small monitors form specifications containing sub-properties of bounded
+temporal scope.
+
+Reference: Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with
+Bounded and Unbounded Future. Proceedings of RV 09, LNCS 5779, 2009.
+
+Author: Lars Kuhtz <[email protected]>
+
+IMPORTANT NOTE:
+
+Please note that MoCS is still prototypic phase. Not all operators are
+supported in all contexts yet. This is not due to limitations of the approach
+but to missing bits in the implementation. If you rely on such a missing bit
+please let us know. Simliar statement holds for the technical quality of the
+generated VHDL Model.
+
+== INSTALLATION FROM SOURCE ==
+
+1. Edit the file config.make
+
+2. To build everything run:
+
+   make all
+
+== USAGE == 
+
+MoCS [--ouput FILE] FILE
+MoCS [--output FILE] --formula STRING
+MoCS [--output FILE]"
+MoCS --help
+MoCS --version
+
+Syntax for a formulas:
+
+--------------------------------------------------------------------------------
+Formula ::= '(' Formula ')' | RegEx | '\strong' Regex 
+         | PrefixOp Formula | BPrefixOp BoundExpr Formula 
+         | Formula BinaryOp Formula | Formula BBinaryOp BoundExpr Formula
+         | Formula '\abort' Prop | RegEx '\simplies' Formula
+
+PrefixOp ::= '\not' | '\N' | '\wN' | '\G' | '\F'
+BPreifxOp ::= '\BN' | '\wBN' | '\BG' | '\BF' | '\sBG' | '\wBF' 
+
+BinaryOp ::= '\and' | '\or' | '\implies' | '\equiv' | '\U' | '\W' | '\R' | '\sR'
+BBinaryOp ::= '\BU' | '\BR' | '\BW' | '\SBR'
+
+Prop ::= '(' Prop ')' | Var | 'true' | 'false' | '-' Prop 
+       | Prop '+' Prop | Prop '^' Prop
+
+RegEx ::= '(' RegEx ')' | Prop | 'epsilon' 
+        | RegEx '&&' RegEx | RegEx '|' RegEx | RegEx ':' RegEx | RegEx ';' RegEx
+        | RegEx '*' | RegEx '[' Ordinal ']'
+
+Var ::= "[_a-zA-Z][_a-zA-Z0-9]*"
+
+BoundExpr ::= '(' BoundExpr ')' | Ordinal
+            | BoundExpr '*' BoundExpr | '-' BoundExpr | BoundExpr '++' 
+
+Ordinal ::= [0-9]+ | 'infty'"
+--------------------------------------------------------------------------------
+