Commit 08694f91 authored by HELOUET Loic's avatar HELOUET Loic
Browse files

commit message

parent 93243efb
Pipeline #314508 failed with stages
in 51 seconds
0;2000.0;499.93546;1437.0588;458.88712;531.6278;
1;2000.0;499.93546;1437.0588;458.88712;531.6278;
2;2000.0;444.00635;1645.242;276.21896;531.6278;
3;2000.0;444.00635;1737.7946;276.21896;531.6278;
4;2000.0;414.79916;1302.9017;276.21896;509.29144;
5;2000.0;414.79916;1297.7145;276.21896;509.29144;
6;2000.0;367.55304;1297.7145;276.21896;458.88712;
7;2000.0;367.55304;1346.6619;276.21896;458.88712;
8;2000.0;276.21896;1346.6619;276.21896;276.21896;
9;2000.0;276.21896;1404.4282;276.21896;276.21896;
10;2000.0;438.1095;1404.4282;276.21896;600.0;
11;2000.0;438.1095;1382.6674;276.21896;600.0;
12;2000.0;492.073;1382.6674;276.21896;600.0;
13;2000.0;492.073;1323.4034;276.21896;600.0;
14;2000.0;438.1095;1323.4034;276.21896;600.0;
15;2000.0;438.1095;1094.1392;276.21896;600.0;
16;2000.0;492.073;1094.1392;276.21896;600.0;
17;2000.0;492.073;1034.6938;276.21896;600.0;
18;2000.0;438.1095;1034.6938;276.21896;600.0;
19;2000.0;438.1095;1039.1359;276.21896;600.0;
20;2000.0;276.21896;1039.1359;276.21896;276.21896;
21;2000.0;276.21896;1078.3013;276.21896;276.21896;
22;2000.0;406.21896;1078.3013;276.21896;276.21896;
23;2000.0;408.21896;1078.3013;276.21896;276.21896;
24;2000.0;409.21896;1078.3013;276.21896;276.21896;
25;2000.0;408.21896;1078.3013;276.21896;276.21896;
26;2000.0;409.21896;1078.3013;276.21896;276.21896;
26;2000.0;309.21896;1078.3013;276.21896;276.21896;
\ No newline at end of file
/** parser specification for MITL formulas */
PARSER_BEGIN(Eg1)
/** An Arithmetic Grammar. */
public class Eg1 {
/** Main entry point. */
public static void main(String args[]) {
System.out.println("Reading from standard input...");
Eg1 t = new Eg1(System.in);
try {
t.Start();
//n.dump("");
System.out.println("Thank you.");
} catch (Exception e) {
System.out.println("Oops.");
System.out.println(e.getMessage());
e.printStackTrace();
}
}
}
PARSER_END(Eg1)
SKIP :
{
" "
| "\t"
| "\n"
| "\r"
| <"//" (~["\n","\r"])* ("\n"|"\r"|"\r\n")>
| <"/*" (~["*"])* "*" (~["/"] (~["*"])* "*")* "/">
}
TOKEN : /* LITERALS */
{
< INTEGER_LITERAL:
<DECIMAL_LITERAL> (["l","L"])?
| <HEX_LITERAL> (["l","L"])?
| <OCTAL_LITERAL> (["l","L"])?
>
|
< #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
|
< #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
|
< #OCTAL_LITERAL: "0" (["0"-"7"])* >
}
TOKEN : /* IDENTIFIERS */
{
<NOT: "NOT">
| <SIGNAL : "Signal">
| < IDENTIFIER: <LETTER> (<LETTER>|<DIGIT>)* >
|
< #LETTER: ["_","a"-"z","A"-"Z"] >
|
< #DIGIT: ["0"-"9"] >
}
/** Main production. */
void Start() : {}
{
Expression()
{ /* When the parser computes a parsing tree, return it here */}
}
/** An Expression. */
void Expression() : {}
{
Signal() | Negation() | Until()
}
/** A signal */
void Signal() : {}
{
<SIGNAL> "(" Identifier() ")"
}
/** Negation */
void Negation() : {}
{
<NOT> "(" Expression() ")"
}
/** Until */
void Until() : {}
{
"(" Expression() Opuntil() Expression() ")"
}
void Opuntil() : {}
{
"U_[" Integer() "," Integer() "]"
}
/** An Identifier. */
void Identifier() : {}
{
<IDENTIFIER>
}
/** An Integer. */
void Integer() : {}
{
<INTEGER_LITERAL>
}
/* Copyright (c) 2006, Sun Microsystems, Inc.
* 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 Sun Microsystems, Inc. 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.
*/
PARSER_BEGIN(Eg1)
/** An Arithmetic Grammar. */
public class Eg1 {
/** Main entry point. */
public static void main(String args[]) {
System.out.println("Reading from standard input...");
Eg1 t = new Eg1(System.in);
try {
SimpleNode n = t.Start();
n.dump("");
System.out.println("Thank you.");
} catch (Exception e) {
System.out.println("Oops.");
System.out.println(e.getMessage());
e.printStackTrace();
}
}
}
PARSER_END(Eg1)
SKIP :
{
" "
| "\t"
| "\n"
| "\r"
| <"//" (~["\n","\r"])* ("\n"|"\r"|"\r\n")>
| <"/*" (~["*"])* "*" (~["/"] (~["*"])* "*")* "/">
}
TOKEN : /* LITERALS */
{
< INTEGER_LITERAL:
<DECIMAL_LITERAL> (["l","L"])?
| <HEX_LITERAL> (["l","L"])?
| <OCTAL_LITERAL> (["l","L"])?
>
|
< #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
|
< #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
|
< #OCTAL_LITERAL: "0" (["0"-"7"])* >
}
TOKEN : /* IDENTIFIERS */
{
< IDENTIFIER: <LETTER> (<LETTER>|<DIGIT>)* >
|
< #LETTER: ["_","a"-"z","A"-"Z"] >
|
< #DIGIT: ["0"-"9"] >
}
/** Main production. */
SimpleNode Start() : {}
{
Expression() ";"
{ return jjtThis; }
}
/** An Expression. */
void Expression() : {}
{
AdditiveExpression()
}
/** An Additive Expression. */
void AdditiveExpression() : {}
{
MultiplicativeExpression() ( ( "+" | "-" ) MultiplicativeExpression() )*
}
/** A Multiplicative Expression. */
void MultiplicativeExpression() : {}
{
UnaryExpression() ( ( "*" | "/" | "%" ) UnaryExpression() )*
}
/** A Unary Expression. */
void UnaryExpression() : {}
{
"(" Expression() ")" | Identifier() | Integer()
}
/** An Identifier. */
void Identifier() : {}
{
<IDENTIFIER>
}
/** An Integer. */
void Integer() : {}
{
<INTEGER_LITERAL>
}
package SLTLVerif;
public class Formula {
// class for Signal LTL formulas
// Core Formulas are of the form
// \phi ::= true | signal(p) | \phi_1 V \phi_2 | \not \phi | \phi_1 U_[a,b] \phi_2
// signal(p) is a boolean signal, given as input, and should appear on a leaf
// true is the boolean signal which is always true in any interval
// Syntactic sugar :
// With easy operator : \phi_1 ^ \phi_2 defined as intersection
// implication : \phi_1 -> \phi_2
//time-constrained eventually operator
// <>_[a,b] \phi ::= true U_[a,b] \phi
// \phi olds at some instant in time interval [a,b]
//time-constrained eventually and always operators
// []_[a,b] \phi ::= \not <>_[a,b] \not \phi
// \phi always holds in time interval [a,b]
// We assume that formulas are well parenthesized, i.e.
//(\phi_1) -> ( (\phi_2) U_[2,3] (\phi_3) ) is correct
// \phi_1 -> \phi_2 U_[2,3] \phi_3 is not
String name; // the name of the formula
String value;
/**
* Creates a parsing tree from a plain text formula
* @return
*/
TreeFormula parse() {
// Formula of the form not ( XX )
}
}
package SLTLVerif;
import java.util.ArrayList;
// The parsing tree of a Signal LTL formula
public class TreeFormula {
TreeNode root; // the root of the tree
String type; // "NOT", "UNTIL", "OR", "AND"
ArrayList<TreeFormula> children; // one or two subtrees depending on the node
String subformula; // the subformula attached to that tree (which parsing is that tree)
TreeFormula(String s, TreeNode n, ArrayList<TreeFormula> c,String t){
root=n;
children=c;
subformula=new String(s);
type = new String(t);
}
/**
* Computed a boolean signal for the current root out of the signals of the children
* The children's signals must have been evaluated before
* @return
*/
booleanSignal buildSignal() {
booleanSignal newSignal= new booleanSignal();
// TODO : use the functions of booleanSignal to compute this new signal
// depending on the type of node
return newSignal;
}
}
package SLTLVerif;
public class TreeNode {
}
......@@ -117,6 +117,27 @@ public class booleanSignal {
booleanSignal intersection(booleanSignal bs2) {
booleanSignal newSignal = new booleanSignal();
for (Interval it2:bs2.positiveParts) { // visit every positive interval in bs2
for (Interval it1:this.positiveParts) { // visit every positive interval in bs2
if (it1.overlap(it2)) {
Interval itv = it1.Intersection(it2);
newSignal.add(itv);
}
}
}
return newSignal;
}
/**
* Sorts positive parts according to their starting date
* Note : we use Java's sorting mechanism which is quite efficient
......@@ -135,12 +156,17 @@ public class booleanSignal {
booleanSignal newSignal = new booleanSignal();
if (this.positiveParts.size() == 0 ) { // if current signal is empty
return newSignal; // return an empty signal
}
// for every interval
// if it overlaps with the next one
// merge both and continue with current interval
// otherwise add
Interval current= this.getFirstInterval();
Interval otherInterval; // the next interval in the list of positiv signals
Interval otherInterval; // the next interval in the list of positive signals
for (int i=1;i<this.positiveParts.size();i++) {
......@@ -157,6 +183,8 @@ public class booleanSignal {
}
newSignal.add(current); // add the last interval open during exploration
return newSignal;
}
......@@ -312,6 +340,19 @@ public class booleanSignal {
bs2.parseFloatField("out.txt", 400, 2, 25);
System.out.println(bs2);
booleanSignal bs3= new booleanSignal();
bs3.parseFloatField("adjacent.txt", 400, 2, 25);
System.out.println("bs3="+ bs3);
booleanSignal bs4 = bs3.union(bs);
System.out.println("bs4= bs U bs3"+ bs4);
System.out.println("bs4 merged ="+ bs4.mergeAdjacent());
booleanSignal bs5 = bs3.intersection(bs2);
System.out.println("bs5= bs2 ^ bs3"+ bs5);
}
......
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