Commit 3c6a3ab1 authored by Christian Müller's avatar Christian Müller

rename examples, add metrics file per case

parent 86f84f77
# /bin/bash
RESULT=results/measure.txt
TIMEOUT=15m
touch ${RESULT}
echo "Measurement $(date)" >> ${RESULT}
echo "" >> ${RESULT}
TIMEOUT=20m
for FILE in results/*.ltl
do
NAME=$(basename ${FILE} .ltl)
METRICS="results/${NAME}.metrics"
echo "Measuring ${FILE}"
echo "${FILE}:" >> ${RESULT}
echo " FOLTL length: $(wc -m < results/${NAME}.foltl)" >> ${RESULT}
echo " LTL length: $(wc -m < ${FILE})" >> ${RESULT}
echo "Metrics File: ${METRICS}"
echo "" >> ${METRICS}
echo "Measuring on $(date):" >> ${METRICS}
# echo " FOLTL length: $(wc -m < results/${NAME}.foltl)" >> ${RESULT}
# echo " LTL length: $(wc -m < ${FILE})" >> ${RESULT}
if
timeout ${TIMEOUT} time -p aalta/Aalta_v2.0/aalta < ${FILE} >> ${RESULT} 2>&1
timeout ${TIMEOUT} time -p aalta/Aalta_v2.0/aalta < ${FILE} >> ${METRICS} 2>&1
then
echo "Finished successfully"
echo " Finished successfully" >> ${RESULT}
echo "Finished successfully" >> ${METRICS}
else
echo "Timeout after ${TIMEOUT}"
echo " Timeout after ${TIMEOUT}" >> ${RESULT}
echo "Timeout after ${TIMEOUT}" >> ${METRICS}
fi
echo "" >> ${RESULT}
done
# /bin/bash
RESULT=results/measure.txt
TIMEOUT=10s
touch ${RESULT}
echo "Measurement $(date)" >> ${RESULT}
echo "" >> ${RESULT}
TIMEOUT=1s
for FILE in results/*.ltl
do
NAME=$(basename ${FILE} .ltl)
METRICS="results/${NAME}.metrics"
echo "Measuring ${FILE}"
echo "${FILE}:" >> ${RESULT}
echo " FOLTL length: $(wc -m < results/${NAME}.foltl)" >> ${RESULT}
echo " LTL length: $(wc -m < ${FILE})" >> ${RESULT}
echo "Metrics File: ${METRICS}"
echo "" >> ${METRICS}
echo "Measuring on $(date):" >> ${METRICS}
# echo " FOLTL length: $(wc -m < results/${NAME}.foltl)" >> ${RESULT}
# echo " LTL length: $(wc -m < ${FILE})" >> ${RESULT}
if
timeout ${TIMEOUT} time -p aalta/Aalta_v2.0/aalta < ${FILE} >> ${RESULT} 2>&1
timeout ${TIMEOUT} time -p aalta/Aalta_v2.0/aalta < ${FILE} >> ${METRICS} 2>&1
then
echo "Finished successfully"
echo " Finished successfully" >> ${RESULT}
echo "Finished successfully" >> ${METRICS}
else
echo "Timeout after ${TIMEOUT}"
echo " Timeout after ${TIMEOUT}" >> ${RESULT}
echo "Timeout after ${TIMEOUT}" >> ${METRICS}
fi
echo "" >> ${RESULT}
done
......@@ -34,8 +34,11 @@ object Main extends App with LazyLogging {
}
def writeExample(name: String, prop: Term) {
var metrics = List[String]()
write(s"${name}.foltl", prop.pretty())
metrics :+= s"${name}.foltl: ${prop.opsize()}"
if (!TermFunctions.checkSanity(prop)) {
logger.error("Property didn't pass sanity check")
......@@ -44,7 +47,8 @@ object Main extends App with LazyLogging {
val (agents, res) = LTL.eliminateExistentials(prop)
logger.info(s"Using universe ${agents.map(_.withType())}")
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
......@@ -53,10 +57,15 @@ object Main extends App with LazyLogging {
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
metrics :+= s"Universe: $universe"
write(s"${name}.ltl", ltlprop.toString())
write(s"${name}.ppltl", ltlprop.pretty())
write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
logger.info(s"Written all files for $name")
}
......@@ -74,6 +83,7 @@ object Main extends App with LazyLogging {
val cprop = Properties.noninterCausal(spec)
writeExample(s"$FOLDER/${name}_causal", cprop)
}
}
// Clear results folder
......
......@@ -14,6 +14,7 @@ object FOLTL {
def in(name: String) = TermFunctions.annotate(this, name)
def in(name: String, ignore: Set[String]) = TermFunctions.annotate(this, name, ignore)
def collect[T](coll: PartialFunction[Term, List[T]]) = TermFunctions.collect(coll, this)
def opsize() = TermFunctions.opsize(this)
def bracketed(): String = this match {
case _: BinOp => "(" + this + ")"
......
......@@ -50,17 +50,16 @@ object TermFunctions extends LazyLogging {
case And(t, True) => t
// Equivalence
case Eq(t1, t2) if t1 == t2 => True
case Eq(t1, t2) if t1 == t2 => True
// Double Temporals
case Finally(Finally(t)) => Finally(t)
case Globally(Globally(t)) => Globally(t)
// Remove quantifiers if empty
case Quantifier(qmake, xs, t) if xs.isEmpty => t
case Quantifier(qmake, xs, True) => True
case Quantifier(qmake, xs, False) => False
case Quantifier(_, xs, t) if xs.isEmpty => t
case Quantifier(_, _, True) => True
case Quantifier(_, _, False) => False
// Remove variables from quantifiers if not used in the body
// case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
......@@ -89,8 +88,18 @@ object TermFunctions extends LazyLogging {
case x => x
}
}
def collect[T](combine:(T*) => T, empty:T)(coll: PartialFunction[Term, T], t: Term): T = {
def opsize(t: Term): Int = {
t match {
// Extractors
case Quantifier(_, ps, t) => 1 + t.opsize()
case UnOp(_, t) => 1 + t.opsize()
case BinOp(_, t1, t2) => 1 + t1.opsize() + t2.opsize()
case x => 1
}
}
def collect[T](combine: (T*) => T, empty: T)(coll: PartialFunction[Term, T], t: Term): T = {
if (coll.isDefinedAt(t))
coll(t)
else
......@@ -102,8 +111,8 @@ object TermFunctions extends LazyLogging {
case x => empty
}
}
def collect[T](coll: PartialFunction[Term, List[T]], t: Term): List[T] = {
def collect[T](coll: PartialFunction[Term, List[T]], t: Term): List[T] = {
if (coll.isDefinedAt(t))
coll(t)
else
......@@ -115,7 +124,7 @@ object TermFunctions extends LazyLogging {
case x => List.empty
}
}
def assumeEmpty(t: Term, name: String) = {
t.everywhere({
case Fun(f, _, _) if f == name => False
......@@ -127,13 +136,13 @@ object TermFunctions extends LazyLogging {
case Fun(f, None, xs) => Fun(f, Some(name), xs)
})
}
def annotate(t: Term, name: String, ignore:Set[String]) = {
def annotate(t: Term, name: String, ignore: Set[String]) = {
t.everywhere({
case Fun(f, None, xs) if (!(ignore contains f)) => Fun(f, Some(name), xs)
})
}
def checkSanity(t: Term) = {
// TODO add more things, f.e. existentials
// T1, T2 can appear freely
......@@ -141,7 +150,7 @@ object TermFunctions extends LazyLogging {
if (!frees.isEmpty) {
logger.warn(s"Sanity check failed: $frees appear free in the property.")
}
frees.isEmpty
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment