Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 18bc86d7 authored by EXT José Ignacio Requeno Jarabo's avatar EXT José Ignacio Requeno Jarabo
Browse files

Work in progress

parent 3db59828
Pipeline #51662 failed with stages
in 60 minutes and 1 second
......@@ -56,12 +56,21 @@ They require as input:
- An index word (alpha) or the i-th component of the index word (alphai),
- The space (xspace).
Paper in [3] introduces a variant of the algorithm presented in [1],
which allows the intersection of two Pareto fronts according to some epsilon count.
Functions for alpha and cube generators are specialized for this case
and are named with 'inter'-*.
[1] Learning Monotone Partitions of Partially-Ordered Domains,
Nicolas Basset, Oded Maler, J.I Requeno, in
doc/article.pdf.
[2] [Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress) 2017.
〈hal-01556243〉] (https://hal.archives-ouvertes.fr/hal-01556243/)
[3] Learning Specifications for Labelled Patterns,
Nicolas Basset, Thao Dang, Akshay Mambakam, J.I Requeno, in
FORMATS 2020: 76-93
"""
import math
......@@ -72,8 +81,9 @@ from itertools import product, tee
import ParetoLib.Geometry as RootGeom
from ParetoLib.Geometry.Segment import Segment
from ParetoLib.Geometry.Point import greater, greater_equal, less, less_equal, equal, add, subtract, div, mult, distance, dim, \
incomparables, select, subt, int_to_bin_tuple, minimum, maximum#, r
from ParetoLib.Geometry.Point import greater, greater_equal, less, less_equal, equal, add, subtract, div, mult, \
distance, dim, \
incomparables, select, subt, int_to_bin_tuple, minimum, maximum # , r
from ParetoLib._py3k import red
from ParetoLib.Search.CommonSearch import EPS
......@@ -582,7 +592,7 @@ class Rectangle(object):
# Besides, the mismatching coordinate must have continuous interval
mismatching_index = corner_eq.index(False)
concatenable = (self.max_corner[mismatching_index] == other.min_corner[mismatching_index]) or \
(other.max_corner[mismatching_index] == self.min_corner[mismatching_index])
(other.max_corner[mismatching_index] == self.min_corner[mismatching_index])
return concatenable
......@@ -892,6 +902,7 @@ class Rectangle(object):
"""
Synonym of intersection(self, other).
"""
def difference(self, other):
# type: (Rectangle, Rectangle) -> iter
"""
......@@ -944,8 +955,8 @@ class Rectangle(object):
# ground = new_ground
# ceil = new_ceil
inner_ground = ground[:i] + (max(ground[i], inter.max_corner[i]),) + ground[i+1:]
inner_ceil = ceil[:i] + (min(ceil[i], inter.min_corner[i]),) + ceil[i+1:]
inner_ground = ground[:i] + (max(ground[i], inter.max_corner[i]),) + ground[i + 1:]
inner_ceil = ceil[:i] + (min(ceil[i], inter.min_corner[i]),) + ceil[i + 1:]
r1 = Rectangle(ground, inner_ceil)
r2 = Rectangle(inner_ground, ceil)
......@@ -955,8 +966,8 @@ class Rectangle(object):
if r2.volume() > 0:
diff_set.add(r2)
ground = ground[:i] + (max(ground[i], inter.min_corner[i]),) + ground[i+1:]
ceil = ceil[:i] + (min(ceil[i], inter.max_corner[i]),) + ceil[i+1:]
ground = ground[:i] + (max(ground[i], inter.min_corner[i]),) + ground[i + 1:]
ceil = ceil[:i] + (min(ceil[i], inter.max_corner[i]),) + ceil[i + 1:]
return list(diff_set)
def difference_func(self, other):
......@@ -1179,10 +1190,10 @@ class Rectangle(object):
if b[i] < clipminc[i]:
b[i] = clipminc[i]
elif b[i] > clipmaxc[i]:
b[i] = clipmaxc[i]
b[i] = clipmaxc[i]
minc = (a[0], a[1], a[2],)
maxc = (b[0], b[1], b[2],)
rect = Rectangle(minc, maxc)
# sorted(vertices) =
......@@ -1350,6 +1361,10 @@ class Rectangle(object):
# Alpha generators
##################
###########
# Standard subclass
###########
def comp(d):
# Set of comparable rectangles
# Particular cases of alpha
......@@ -1368,7 +1383,11 @@ def incomp(d, opt=True):
else:
return incomp_expanded(d)
###########
# Intersection subclass
###########
# TODO: @Akshay, explain this 'NOTE'
'''
NOTE:
0 -> a
......@@ -1378,48 +1397,56 @@ NOTE:
4 -> (b+c)
5 -> (a+b+c)
'''
def incomp_segmentNegRemoveDown(d):
if d > 0:
return incomp_segmentNegRemoveDownE(d)
else:
return []
def incomp_segmentNegRemoveDownE(d):
if(d == 0):
if d == 0:
return []
else:
elist = ["0" + i for i in incomp_segmentNegRemoveDownE(d-1)]
elist += ["1" + ('3')*(d-1)]
elist = ["0" + i for i in incomp_segmentNegRemoveDownE(d - 1)]
elist += ["1" + ('3') * (d - 1)]
return elist
def incomp_segmentNegRemoveUp(d):
if d > 0:
return incomp_segmentNegRemoveUpE(d)
else:
return []
def incomp_segmentNegRemoveUpE(d):
if(d == 0):
if (d == 0):
return []
else:
elist = ["1" + i for i in incomp_segmentNegRemoveUpE(d-1)]
elist += ["0" + ('3')*(d-1)]
elist = ["1" + i for i in incomp_segmentNegRemoveUpE(d - 1)]
elist += ["0" + '3' * (d - 1)]
return elist
def incomp_segmentpos(d):
if d > 0:
return incomp_segmentposE(d)
else:
return []
def incomp_segmentposE(d):
if (d == 0):
if d == 0:
return []
else:
elist1 = ["1" + i for i in incomp_segmentposE(d-1)]
elistDown = ["0" + ('5')*(d-1)]
elistUp = ["2" + ('5')*(d-1)]
return elistDown+elistUp+elist1
elist1 = ["1" + i for i in incomp_segmentposE(d - 1)]
elistDown = ["0" + '5' * (d - 1)]
elistUp = ["2" + '5' * (d - 1)]
return elistDown + elistUp + elist1
def incomp_segment(d):
if d > 0:
......@@ -1427,30 +1454,35 @@ def incomp_segment(d):
else:
return []
def incomp_segmentE(d):
if (d == 1):
if d == 1:
return []
else:
elist = ["0" + i for i in incomp_segmentC(d-1)] + ["2" + i for i in incomp_segmentA(d-1)]
elist += ["1" + i for i in incomp_segmentE(d-1)]
elist = ["0" + i for i in incomp_segmentC(d - 1)] + ["2" + i for i in incomp_segmentA(d - 1)]
elist += ["1" + i for i in incomp_segmentE(d - 1)]
return elist
def incomp_segmentA(d):
if (d == 1):
if d == 1:
return ["0"]
else:
alist = ["0" + ('5')*(d-1)]
alist += ["4" + i for i in incomp_segmentA(d-1)]
alist = ["0" + '5' * (d - 1)]
alist += ["4" + i for i in incomp_segmentA(d - 1)]
return alist
def incomp_segmentC(d):
if (d == 1):
if d == 1:
return ["2"]
else:
clist = ["2" + ('5')*(d-1)]
clist += ["3" + i for i in incomp_segmentC(d-1)]
clist = ["2" + '5' * (d - 1)]
clist += ["3" + i for i in incomp_segmentC(d - 1)]
return clist
###########
def incomp_expanded(d):
# type: (int) -> list
alphaprime = (range(2),) * d
......@@ -1492,6 +1524,8 @@ def E(d):
#################
# Cube generators
#################
# inter-functions are the reimplementation of the standard cube generators for the intersection algorithm
def intercpoint(i, alphai, yspace, xspace):
# type: (int, int, tuple, Rectangle) -> Rectangle
result_xspace = Rectangle(xspace.min_corner, xspace.max_corner)
......@@ -1511,10 +1545,11 @@ def intercpoint(i, alphai, yspace, xspace):
result_xspace.min_corner = subt(i, xspace.min_corner, yspace.min_corner)
# result_xspace.max_corner = subt(i, xspace.max_corner, xspace.max_corner)
# elif alpha == '5': # Nothing to be done here.
# result_xspace.min_corner = subt(i, xspace.min_corner, xspace.min_corner)
# result_xspace.max_corner = subt(i, xspace.max_corner, xspace.max_corner)
# result_xspace.min_corner = subt(i, xspace.min_corner, xspace.min_corner)
# result_xspace.max_corner = subt(i, xspace.max_corner, xspace.max_corner)
return result_xspace
def cpoint(i, alphai, ypoint, xspace):
# type: (int, int, tuple, Rectangle) -> Rectangle
result_xspace = Rectangle(xspace.min_corner, xspace.max_corner)
......@@ -1526,12 +1561,13 @@ def cpoint(i, alphai, ypoint, xspace):
result_xspace.min_corner = subt(i, xspace.min_corner, ypoint)
return result_xspace
def intercrect(i, alphai, yrectangle, xspace):
# type: (int, int, Rectangle, Rectangle) -> Rectangle
result_xspace = Rectangle(xspace.min_corner, xspace.max_corner)
result_xspace = intercpoint(i, alphai, yrectangle, xspace)
return result_xspace
def crect(i, alphai, yrectangle, xspace):
# type: (int, int, Rectangle, Rectangle) -> Rectangle
result_xspace = Rectangle(xspace.min_corner, xspace.max_corner)
......@@ -1555,6 +1591,7 @@ def bpoint(alpha, ypoint, xspace):
temp = cpoint(i, alphai, ypoint, temp)
return temp
def interbrect(alpha, yrectangle, xspace):
# type: (tuple, Rectangle, Rectangle) -> Rectangle
assert (dim(yrectangle.min_corner) == dim(yrectangle.max_corner)), \
......@@ -1572,6 +1609,7 @@ def interbrect(alpha, yrectangle, xspace):
temp = intercrect(i, alphai, yrectangle, temp)
return temp
def brect(alpha, yrectangle, xspace):
# type: (tuple, Rectangle, Rectangle) -> Rectangle
assert (dim(yrectangle.min_corner) == dim(yrectangle.max_corner)), \
......@@ -1589,6 +1627,7 @@ def brect(alpha, yrectangle, xspace):
temp = crect(i, alphai, yrectangle, temp)
return temp
def interirect(alphaincomp, yrectangle, xspace):
# type: (list, Rectangle, Rectangle) -> list
assert (dim(yrectangle.min_corner) == dim(yrectangle.max_corner)), \
......@@ -1601,6 +1640,7 @@ def interirect(alphaincomp, yrectangle, xspace):
# 'alphaincomp_list and yrectangle.max_corner do not share the same dimension'
return [interbrect(alphaincomp_i, yrectangle, xspace) for alphaincomp_i in alphaincomp]
def irect(alphaincomp, yrectangle, xspace):
# type: (list, Rectangle, Rectangle) -> list
assert (dim(yrectangle.min_corner) == dim(yrectangle.max_corner)), \
......@@ -1620,8 +1660,8 @@ def idwc(y, z):
# y = [0, y_]
# assert y.min_corner <= z.min_corner, 'Minimal corner of {0} must be at the origin of the xspace ' \
# '(i.e., {0} <= {1})'.format(y.min_corner, z.min_corner)
assert less_equal(y.min_corner, z.min_corner) or incomparables(y.min_corner, z.min_corner),\
'Minimal corner of {0} must be at the origin of the xspace (i.e., {0} <= {1})'\
assert less_equal(y.min_corner, z.min_corner) or incomparables(y.min_corner, z.min_corner), \
'Minimal corner of {0} must be at the origin of the xspace (i.e., {0} <= {1})' \
.format(y.min_corner, z.min_corner)
# assert z.min_corner <= y.max_corner, 'Rectangles {0} and {1} must intersect'.format(y, z)
assert less_equal(z.min_corner, y.max_corner) or incomparables(z.min_corner, y.max_corner), \
......@@ -1630,14 +1670,14 @@ def idwc(y, z):
def w_set(m):
# type: (int) -> iter
# { 0^{j-1} 1 *^{m-j} } for j in [1, m]
return ["0"*(j-1) + "1" + "*"*(m-j) for j in range(1, m+1)]
return ["0" * (j - 1) + "1" + "*" * (m - j) for j in range(1, m + 1)]
def gamma(w, y, z):
# type: (iter, Rectangle, Rectangle) -> tuple
d = z.dim()
j = 0
alpha = ["*"]*d
alpha = ["*"] * d
for i in range(d):
if y.max_corner[i] < z.max_corner[i]:
alpha[i] = w[j]
......@@ -1669,7 +1709,7 @@ def iuwc(y, z):
# assert z.max_corner <= y.max_corner, 'Maximal corner of {1} must be the highest value of the xspace ' \
# '(i.e., {0} <= {1})'.format(y.min_corner, z.min_corner)
assert less_equal(z.max_corner, y.max_corner) or incomparables(z.max_corner, y.max_corner), \
'Maximal corner of {1} must be the highest value of the xspace (i.e., {0} <= {1})'\
'Maximal corner of {1} must be the highest value of the xspace (i.e., {0} <= {1})' \
.format(y.min_corner, z.min_corner)
# assert y.min_corner <= z.max_corner, 'Rectangles {0} and {1} must intersect'.format(y, z)
assert less_equal(y.min_corner, z.max_corner) or incomparables(y.min_corner, z.max_corner), \
......@@ -1678,14 +1718,14 @@ def iuwc(y, z):
def w_set(m):
# type: (int) -> iter
# { 1^{j-1} 0 *^{m-j} } for j in [1, m]
return ["1"*(j-1) + "0" + "*"*(m-j) for j in range(1, m+1)]
return ["1" * (j - 1) + "0" + "*" * (m - j) for j in range(1, m + 1)]
def gamma(w, y, z):
# type: (iter, Rectangle, Rectangle) -> tuple
d = z.dim()
j = 0
alpha = ["*"]*d
alpha = ["*"] * d
for i in range(d):
# if y.min_corner[i] < z.max_corner[i]:
if z.min_corner[i] < y.min_corner[i]:
......
......@@ -2,49 +2,47 @@ import ParetoLib.Oracle as RootOracle
from ParetoLib.Oracle.OracleSTLe import OracleSTLeLib
from ParetoLib.STLe.STLe import MAX_STLE_CALLS
import os
def countEpsilonSeparated(intervalList, epsilon):
# type: (list, float) -> int
if len(intervalList) == 0:
return 0
startOfTime = 0
cardinality = 0
i = 0
(beginOfEnd, end) = intervalList[-1]
startOfTime = 0
startOfTime = 0.0
epsCoveringSize = 0
currentIndex = 0
while currentIndex < len(intervalList):
oldStartOfTime = startOfTime
(currentIndex, startOfTime) = moveTimeNeedleByEpsilon(intervalList, epsilon, currentIndex, startOfTime)
epsCoveringSize += 1
return epsCoveringSize
def moveTimeNeedleByEpsilon(intervalList, epsilon, currentIndex, startOfTime):
if(startOfTime == intervalList[currentIndex][1]):
return (currentIndex + 1, startOfTime)
# type: (list, float, int, float) -> (int, float)
if startOfTime == intervalList[currentIndex][1]:
return currentIndex + 1, startOfTime
(tBegin, tEnd) = intervalList[currentIndex]
if(startOfTime < tBegin):
if startOfTime < tBegin:
startOfTime = tBegin
i = currentIndex
while i < len(intervalList) and (startOfTime + epsilon) >= intervalList[i][1]:
i += 1
return i, startOfTime + epsilon
class OracleEpsSTLe(OracleSTLeLib):
def __init__(self, boundOnCount, intvlEpsilon=5, stl_prop_file='', csv_signal_file='', stl_param_file=''):
# type: (OracleEpsSTLe, str, str, str) -> None
# type: (OracleEpsSTLe, int, int, str, str, str) -> None
"""
Initialization of Oracle.
OracleSTLeLib interacts directly with the C library of STLe via the C API that STLe exports.
OracleSTLeLib should be usually faster than OracleSTLe
This class is an extension of the STLe oracle.
It is intended for computing the size of minimal epsilon covering.
It is intended for computing the size of minimal epsilon covering.
"""
OracleSTLeLib.__init__(self, stl_prop_file, csv_signal_file, stl_param_file)
self.epsilon = intvlEpsilon
self.bound = boundOnCount
self.bound = boundOnCount
def member(self, xpoint):
# type: (OracleEpsSTLe, tuple) -> bool
......@@ -59,54 +57,9 @@ class OracleEpsSTLe(OracleSTLeLib):
# Replace parameters of the STL formula with current values in xpoint tuple
val_stl_formula = self._replace_val_stl_formula(xpoint)
# Invoke STLe for solving the STL formula for the current values for the parameters
result = False
self.num_oracle_calls = self.num_oracle_calls + 1
epsSeparationSize = 0
if(1):
epsSeparationSize = self.eps_separate_stl_formula(val_stl_formula, self.epsilon)
else:
outContent = self.gen_result(val_stl_formula)
# get the interval list.
intvlList = self.get_interval_list(outContent)
# compute the count, compare and return.
#print 'epsSeparationSize:', epsSeparationSize, 'bound:', self.bound
# Invoke STLe for solving the STL formula for the current values for the parameters
epsSeparationSize = self.eps_separate_stl_formula(val_stl_formula, self.epsilon)
return epsSeparationSize <= self.bound
#return countEpsilonSeparated(intvlList, 1) < self.bound
def get_interval_list(self, outContent):
outLines = outContent.split('\n')
intvlList = []
seen = False
intvlStart = 0
for line in outLines:
parts = line.split(' ')
timeStamp = parts[0].strip()
boolVal = parts[1].strip()
if seen:
intvlEnd = float(timeStamp)
intvlList.append((intvlStart, intvlEnd))
seen = False
elif(boolVal == '1'):
intvlStart = float(timeStamp)
seen = True
return intvlList
def gen_result(self, val_stl_formula):
outfname = 'quickEtdirty'
# Run the property
stle_path = '/home/akshay/Documents/examples/stle'
stleCmd=stle_path+' '+self.csv_signal_file+' -f "'+val_stl_formula+'" -os 1 -osf g -osn "tub" > localmax_max.txt'
os.system(stleCmd)
# Read the output
readFile = open('localmax_max.txt', 'r')
fileContent = readFile.read()
readFile.close()
outContent = fileContent[fileContent.find('tub"')+4:fileContent.find('"tub points')]
outContent = outContent.strip()
return outContent
\ No newline at end of file
import io, os
import ParetoLib.Oracle as RootOracle
from ParetoLib.Oracle.Oracle import Oracle
from ParetoLib.Oracle.OracleSTLe import OracleSTLeLib
from ParetoLib.Oracle.OracleEpsSTLe import OracleEpsSTLe
from ParetoLib.Search.Search import SearchIntersection2D, SearchIntersection3D, Search2D, EPS, DELTA, STEPS
from ParetoLib.Search.Search import SearchIntersection3D, EPS, DELTA, STEPS
# NOTE: This is actually not an Oracle but an Example:
# '__init__' corresponds to the definition of parameters
# 'member' corresponds to the initialization of the OracleEpsSTLe
class OracleFnFp3D(Oracle):
def __init__(self, scratchDir, ecgFile, min_tuple, max_tuple, queryDelta):
......@@ -16,114 +16,93 @@ class OracleFnFp3D(Oracle):
self.min_tuple = min_tuple
self.max_tuple = max_tuple
self.queryDelta = queryDelta
nfile1 = self.runDir+'/ecgLearn1.txt'
nfile2 = self.runDir+'/ecgLearn2.txt'
#nfile1 = '../../Tests/Oracle/OracleFunction/2D/test1_1.txt'
#nfile2 = '../../Tests/Oracle/OracleFunction/2D/test1_2.txt'
scratch_name1 = '/scratch_fn3D.stl'
scratch_name2 = '/scratch_fp3D.stl'
scratch_file1 = self.runDir + scratch_name1
scratch_file2 = self.runDir + scratch_name2
paramFile = open(self.runDir+'/ecgLearn.param', 'w')
nfile1 = self.runDir + '/ecgLearn1.txt'
nfile2 = self.runDir + '/ecgLearn2.txt'
# nfile1 = '../../Tests/Oracle/OracleFunction/2D/test1_1.txt'
# nfile2 = '../../Tests/Oracle/OracleFunction/2D/test1_2.txt'
scratch_name1 = '/scratch_fn3D.stl'
scratch_name2 = '/scratch_fp3D.stl'
paramFile = open(self.runDir + '/ecgLearn.param', 'w')
for i in range(3):
print >>paramFile, 'p'+str(i+1)
paramFile.write('p' + str(i + 1))
paramFile.close()
controlFile = open(nfile1, 'w')
controlText = ''
print >>controlFile, self.runDir+scratch_name1
print >>controlFile, self.runDir+"/"+self.ecgFile
print >>controlFile, self.runDir+'/ecgLearn.param'
controlFile.write('{0}{1}'.format(self.runDir, scratch_name1))
controlFile.write('{0}/{1}'.format(self.runDir, self.ecgFile))
controlFile.write('{0}/{1}'.format(self.runDir, 'ecgLearn.param'))
controlFile.close()
controlFile = open(nfile2, 'w')
controlText = ''
print >>controlFile, self.runDir+scratch_name2
print >>controlFile, self.runDir+"/"+self.ecgFile
print >>controlFile, self.runDir+'/ecgLearn.param'
controlFile = open(nfile2, 'w')
controlFile.write('{0}{1}'.format(self.runDir, scratch_name2))
controlFile.write('{0}/{1}'.format(self.runDir, self.ecgFile))
controlFile.write('{0}/{1}'.format(self.runDir, 'ecgLearn.param'))
controlFile.close()
def member(self, point):
print 'Point Here:', point
print '------------------------------------'
nfile1 = self.runDir+'/ecgLearn1.txt'
nfile2 = self.runDir+'/ecgLearn2.txt'
template_file1 = self.runDir + '/template_fn3D.stl'
template_file2 = self.runDir + '/template_fp3D.stl'
scratch_name1 = '/scratch_fn3D.stl'
scratch_name2 = '/scratch_fp3D.stl'
scratch_file1 = self.runDir + scratch_name1
scratch_file2 = self.runDir + scratch_name2
temp_file = open(template_file1, 'r')
temp_string = temp_file.read()
# temp_string = temp_string.replace('num_fn',str(point[0]))
temp_file.close()
temp_file = open(scratch_file1, 'w')
temp_file.write(temp_string)
temp_file.close()
temp_file = open(template_file2, 'r')
temp_string = temp_file.read()
# temp_string = temp_string.replace('num_fp',str(point[1]))
temp_file.close()
temp_file = open(scratch_file2, 'w')
temp_file.write(temp_string)
temp_file.close()
RootOracle.logger.debug('Point Here: {0}'.format(point))
RootOracle.logger.debug('------------------------------------')
nfile1 = self.runDir + '/ecgLearn1.txt'
nfile2 = self.runDir + '/ecgLearn2.txt'
template_file1 = self.runDir + '/template_fn3D.stl'
template_file2 = self.runDir + '/template_fp3D.stl'
scratch_name1 = '/scratch_fn3D.stl'
scratch_name2 = '/scratch_fp3D.stl'
scratch_file1 = self.runDir + scratch_name1
scratch_file2 = self.runDir + scratch_name2
temp_file = open(template_file1, 'r')
temp_string = temp_file.read()
# temp_string = temp_string.replace('num_fn',str(point[0]))
temp_file.close()
temp_file = open(scratch_file1, 'w')
temp_file.write(temp_string)
temp_file.close()
temp_file = open(template_file2, 'r')
temp_string = temp_file.read()
# temp_string = temp_string.replace('num_fp',str(point[1]))
temp_file.close()
temp_file = open(scratch_file2, 'w')
temp_file.write(temp_string)
temp_file.close()
temp_file = None
human_readable = True
min_x, min_y, min_z = self.min_tuple