Commit 8335cfd5 authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'master' into parser

parents b55e4e1a 9cf45a69
......@@ -21,6 +21,7 @@ tiamo: src/main.native
src/main.native: src/timedAutomatonBuilder.o
.ml.native:
rm -f $(BUILDDIR)/$@
XML_LINK_FLAGS="$(XML_LIBS)" CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -pkg udbml -lflags "-cclib -L$(UPPAAL_DIR) -cclib -ludbm" $@
.c.o:
......@@ -29,3 +30,12 @@ src/main.native: src/timedAutomatonBuilder.o
clean-local:
$(OCAMLBUILD) -clean
rm -f tiamo
# test part
TEST_EXTENSIONS = .data
DATA_LOG_COMPILER = ./run_test.pl
TESTS = \
tests/test_1.data
#! /usr/bin/perl
print "Running test : $ARGV[0] \n";
open IN, "< $ARGV[0]";
my $title = <IN>;
chomp $title;
my $call = <IN>;
chomp $call;
my $nominal ;
while (my $line = <IN>) {
if ($line =~ /Result of verification/) {
$nomimal = $line;
last;
}
}
close IN;
# Now run the tool#
# print "syscalling : $call \n";
print "##teamcity[testStarted name='$title']\n";
my $tested;
my @outputs = ();
my @results = `$call`;
while (my $line = shift(@results)) {
push (@outputs,$line);
if ($line =~ /Result of verification/) {
$tested = $line;
last;
}
}
# retrieve the exit value of the test
my $failure;
if ($? == 0) {
$failure = 0;
} else {
$failure = 1;
}
my $returnvalue;
if ( $nominal != $tested ) {
print "@outputs\n";
print "\n##teamcity[testFailed name='$title' message='regression detected' details='' expected='$nominal' actual='$tested'] \n";
print "Expected : $nominal Obtained : $tested \n";
$returnvalue = 1;
} elsif ( $failure ) {
print "@outputs\n";
print "\n##teamcity[testFailed name='$title' message='test did not exit properly' details='' expected='$nominal' actual='$tested'] \n";
print "Expected : $nominal Obtained : $tested \n";
my $exitval = $? >> 8;
print "test exited with value $exitval\n";
$returnvalue = 99;
} else {
# print "##teamcity[buildStatisticValue key='testDuration' value='@tested[2]']\n";
# print "##teamcity[buildStatisticValue key='testMemory' value='@tested[3]']\n";
print "Test successful : $title \n";
print "Control Values/Obtained : \n$title\n$nominal\n$tested\n";
$returnvalue = 0;
}
print "##teamcity[testFinished name='$title']\n";
exit $returnvalue;
......@@ -208,12 +208,16 @@ struct
let model =
let ta = BareTA.model in
let clocks = VarContext.create () in
(* the reference clock *)
let _ = VarContext.add clocks "t(0)" in
for i = 1 to BareTA.nb_clocks ta do
let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
assert(i = j)
done;
(* the reference clock *)
let _ =
try
VarContext.add clocks "t(0)"
with Var_already_defined -> -1 (* OK, uppaalta already defines t(0) *)
in
{
t = BareTA.model;
clocks = clocks;
......
......@@ -359,11 +359,54 @@ make_query(const expression_t &query)
CAMLreturn(result);
}
// transforms an assignment 'e @= f' into 'e = e @ f'
// where @ is one of +,-,*,/
expression_t
normalize_assignment(const expression_t &update)
{
switch (update.getKind())
{
case Constants::ASSPLUS:
case Constants::ASSMINUS:
case Constants::ASSMULT:
case Constants::ASSDIV:
{
expression_t new_rhs;
Constants::kind_t op;
switch (update.getKind())
{
case Constants::ASSPLUS:
op = Constants::PLUS;
break;
case Constants::ASSMINUS:
op = Constants::MINUS;
break;
case Constants::ASSMULT:
op = Constants::MULT;
break;
case Constants::ASSDIV:
op = Constants::DIV;
break;
default: // cannot happen
assert(false);
throw "cannot happen";
}
new_rhs = expression_t::createBinary(op, update[0], update[1]);
return expression_t::createBinary(Constants::ASSIGN, update[0], new_rhs);
}
default:
return update;
}
}
extern "C" CAMLprim value
make_update(value process, const expression_t &update)
make_update(value process, const expression_t &u)
{
CAMLparam1(process);
CAMLlocal4(result, lhs, rhs, tmp);
// remove compound assignments (+=, -=, *=, /=)
expression_t update = normalize_assignment(u);
result = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
switch (update.getKind())
{
......
......@@ -472,7 +472,8 @@ struct
let nb_clocks ta = VarContext.size (clocks ta)
let string_of_clock ta cl =
VarContext.var_of_index (clocks ta) cl
assert(cl > 0 && cl <= nb_clocks ta);
VarContext.var_of_index (clocks ta) (cl-1)
let initial_state ta = ta.init
......
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
<nta>
<declaration>// Place global declarations here.</declaration>
<template>
<name x="5" y="5">Template</name>
<declaration>// Place local declarations here.
int x = 0;</declaration>
<location id="id0" x="-365" y="8">
<name x="-375" y="-26">truc</name>
</location>
<location id="id1" x="0" y="0">
</location>
<init ref="id1"/>
<transition>
<source ref="id0"/>
<target ref="id1"/>
<label kind="assignment" x="-187" y="93">x += 1</label>
<nail x="-161" y="93"/>
</transition>
<transition>
<source ref="id1"/>
<target ref="id0"/>
<label kind="assignment" x="-212" y="-17">x -= 1</label>
</transition>
</template>
<system>// Place template instantiations here.
Process = Template();
// List one or more processes to be composed into a system.
system Process;
</system>
<queries>
<query>
<formula>E&lt;&gt; Process.truc
</formula>
<comment>
</comment>
</query>
</queries>
</nta>
Simple Reachability, default options
./tiamo reach tests/bla.xml
Input automaton parsed, computing LU bounds
discrete states: 2
states seen: 2
states explored: 1
max size of storage: 2
incl tests: 0
pos. incl tests: 0
Result of verification is Reachable!
Path is
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