Skip to content

Commit

Permalink
[examples] added simple tube paving (1d)
Browse files Browse the repository at this point in the history
  • Loading branch information
SimonRohou committed Mar 16, 2021
1 parent 0996ca9 commit bed28ab
Show file tree
Hide file tree
Showing 7 changed files with 184 additions and 44 deletions.
2 changes: 2 additions & 0 deletions examples/CMakeLists.txt
Expand Up @@ -87,6 +87,8 @@ if(BUILD_TESTS AND TEST_EXAMPLES)
add_test(NAME basics_07_py
COMMAND python3 ${CMAKE_CURRENT_SOURCE_DIR}/basics/07_temporal_ctc/07_temporal_ctc.py 0)
endif()
add_test(NAME basics_08
COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/basics/08_tubepaving/build/codac_basics_08 0)

# Robotics
add_test(NAME rob_01
Expand Down
41 changes: 41 additions & 0 deletions examples/basics/08_tube_paving/CMakeLists.txt
@@ -0,0 +1,41 @@
# ==================================================================
# codac / basics example - cmake configuration file
# ==================================================================

cmake_minimum_required(VERSION 3.0.2)
project(codac_basics_08 LANGUAGES CXX)

# Adding IBEX

# In case you installed IBEX in a local directory, you need
# to specify its path with the CMAKE_PREFIX_PATH option.
# set(CMAKE_PREFIX_PATH "~/ibex-lib/build_install")

find_package(IBEX REQUIRED)
ibex_init_common() # IBEX should have installed this function
message(STATUS "Found IBEX version ${IBEX_VERSION}")

# Adding Eigen3

# In case you installed Eigen3 in a local directory, you need
# to specify its path with the CMAKE_PREFIX_PATH option, e.g.
# set(CMAKE_PREFIX_PATH "~/eigen/build_install")

find_package(Eigen3 REQUIRED NO_MODULE)
message(STATUS "Found Eigen3 version ${EIGEN3_VERSION}")

# Adding Codac

# In case you installed Codac in a local directory, you need
# to specify its path with the CMAKE_PREFIX_PATH option.
# set(CMAKE_PREFIX_PATH "~/codac/build_install")

find_package(CODAC REQUIRED)
message(STATUS "Found Codac version ${CODAC_VERSION}")

# Compilation

add_executable(${PROJECT_NAME} main.cpp)
target_compile_options(${PROJECT_NAME} PUBLIC ${CODAC_CXX_FLAGS})
target_include_directories(${PROJECT_NAME} SYSTEM PUBLIC ${CODAC_INCLUDE_DIRS} ${EIGEN3_INCLUDE_DIRS})
target_link_libraries(${PROJECT_NAME} PUBLIC ${CODAC_LIBRARIES} Ibex::ibex ${CODAC_LIBRARIES})
11 changes: 11 additions & 0 deletions examples/basics/08_tube_paving/build.sh
@@ -0,0 +1,11 @@
# ==================================================================
# tubex-lib - build script
# ==================================================================

#!/bin/bash

mkdir build -p
cd build
cmake ..
make
cd ..
75 changes: 75 additions & 0 deletions examples/basics/08_tube_paving/main.cpp
@@ -0,0 +1,75 @@
/**
* Codac - Examples
* Tube paving
* ----------------------------------------------------------------------------
*
* \brief Tube paving
* \date 2021
* \author Simon Rohou
* \copyright Copyright 2021 Codac Team
* \license This program is distributed under the terms of
* the GNU Lesser General Public License (LGPL).
*/

#include <codac.h>

using namespace std;
using namespace codac;

class TemporalPaving : public Paving
{
public:

TemporalPaving(const IntervalVector& init_box) : Paving(init_box, SetValue::UNKNOWN)
{

}

void compute(float precision, const Tube& x)
{
assert(precision > 0.);
const Interval& t = box()[0], &y = box()[1];

if(!x(t).intersects(y))
return set_value(SetValue::OUT);

pair<Interval,Interval> p = x.eval(t);

if((p.first == NEG_INFINITY || p.first.ub() < y.lb())
&& (p.second == POS_INFINITY || p.second.lb() > y.ub()))
return set_value(SetValue::IN);

if(box().max_diam() < precision)
return set_value(SetValue::UNKNOWN);

else
{
bisect();
((TemporalPaving*)m_first_subpaving)->compute(precision, x);
((TemporalPaving*)m_second_subpaving)->compute(precision, x);
}
}
};

int main()
{
float dt = 0.005;
Interval tdomain(0,6);
Tube x(tdomain, dt, TFunction("sin(t)+(t+1)*[-0.1,0.1]"));
x.set(Interval(-1.6,1.6),Interval(3,4));

clock_t t_start = clock();
TemporalPaving paving(IntervalVector({{-1,7},{-2,2}}));
x.enable_synthesis(true);
paving.compute(dt*2.,x);
printf("Paving computation time: %.2fs\n", (double)(clock() - t_start)/CLOCKS_PER_SEC);

vibes::beginDrawing();
VIBesFigPaving fig_paving("Paving", &paving);
fig_paving.set_properties(100, 100, 800, 400);
fig_paving.show();
vibes::endDrawing();

return EXIT_SUCCESS;
}
43 changes: 21 additions & 22 deletions src/core/domains/slice/codac_Slice.cpp
Expand Up @@ -175,34 +175,33 @@ namespace codac

const pair<Interval,Interval> Slice::eval(const Interval& t) const
{
if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
return make_pair(Interval::all_reals(), Interval::all_reals());
pair<Interval,Interval> p_eval = make_pair(Interval::empty_set(), Interval::empty_set());

else
if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
{
pair<Interval,Interval> p_eval = make_pair(Interval::empty_set(), Interval::empty_set());

if(t.contains(m_tdomain.lb()))
{
p_eval.first |= input_gate().lb();
p_eval.second |= input_gate().ub();
}
p_eval.first |= NEG_INFINITY;
p_eval.second |= POS_INFINITY;
}

if(t.contains(m_tdomain.ub()))
{
p_eval.first |= output_gate().lb();
p_eval.second |= output_gate().ub();
}
if(t.contains(tdomain().lb()))
{
p_eval.first |= input_gate().lb();
p_eval.second |= input_gate().ub();
}

if(!t.is_degenerated()
|| (t != m_tdomain.lb() && t != m_tdomain.ub()))
{
p_eval.first |= m_codomain.lb();
p_eval.second |= m_codomain.ub();
}
if(t.contains(tdomain().ub()))
{
p_eval.first |= output_gate().lb();
p_eval.second |= output_gate().ub();
}

return p_eval;
if(t.is_subset(tdomain()))
{
p_eval.first |= m_codomain.lb();
p_eval.second |= m_codomain.ub();
}

return p_eval;
}

const Interval Slice::interpol(double t, const Slice& v) const
Expand Down
24 changes: 14 additions & 10 deletions src/core/domains/tube/codac_Tube.cpp
Expand Up @@ -342,13 +342,13 @@ namespace codac

Slice* Tube::slice(int slice_id)
{
assert(slice_id >= 0 && slice_id < nb_slices());
return const_cast<Slice*>(static_cast<const Tube&>(*this).slice(slice_id));
}

const Slice* Tube::slice(int slice_id) const
{
assert(slice_id >= 0 && slice_id < nb_slices());
if(slice_id < 0 && slice_id >= nb_slices())
return NULL;

if(m_synthesis_tree != NULL) // fast access
return m_synthesis_tree->slice(slice_id);
Expand All @@ -370,13 +370,13 @@ namespace codac

Slice* Tube::slice(double t)
{
assert(tdomain().contains(t));
return const_cast<Slice*>(static_cast<const Tube&>(*this).slice(t));
}

const Slice* Tube::slice(double t) const
{
assert(tdomain().contains(t));
if(!tdomain().contains(t))
return NULL;

if(m_synthesis_tree != NULL) // fast evaluation
return m_synthesis_tree->slice(t);
Expand Down Expand Up @@ -672,16 +672,20 @@ namespace codac

else
{
if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
return make_pair(Interval::all_reals(), Interval::all_reals());

pair<Interval,Interval> enclosed_bounds
= make_pair(Interval::EMPTY_SET, Interval::EMPTY_SET);

const Slice *s = slice(t.lb());
while(s != NULL && s->tdomain().lb() <= t.ub())
if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
{
enclosed_bounds.first |= NEG_INFINITY;
enclosed_bounds.second |= POS_INFINITY;
}

Interval t_tdomain = t & tdomain();
const Slice *s = slice(t_tdomain.lb());
while(s != NULL && s->tdomain().lb() <= t_tdomain.ub())
{
pair<Interval,Interval> local_eval = s->eval(t & s->tdomain());
pair<Interval,Interval> local_eval = s->eval(t_tdomain & s->tdomain());
enclosed_bounds.first |= local_eval.first;
enclosed_bounds.second |= local_eval.second;
s = s->next_slice();
Expand Down
32 changes: 20 additions & 12 deletions src/core/domains/tube/codac_TubeTreeSynthesis.cpp
Expand Up @@ -152,44 +152,52 @@ namespace codac

const pair<Interval,Interval> TubeTreeSynthesis::eval(const Interval& t)
{
pair<Interval,Interval> p = make_pair(Interval::EMPTY_SET, Interval::EMPTY_SET);

if(t.is_degenerated()) // faster to perform the evaluation over the related slice
return slice(time_to_index(t.lb()))->eval(t);
p = slice(time_to_index(t.lb()))->eval(t);

if(t.is_empty())
return make_pair(Interval::empty_set(), Interval::empty_set());

else if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
return make_pair(Interval::all_reals(), Interval::all_reals());
else if(t.is_empty())
p = make_pair(Interval::empty_set(), Interval::empty_set());

else if(is_leaf() || t == m_tdomain) // todo: this last condition useful?
{
if(t == m_tdomain)
return codomain_bounds();
p = codomain_bounds();

else
return m_slice_ref->eval(t);
p = m_slice_ref->eval(t & m_tdomain);
}

else
else if(t.intersects(tdomain()))
{
Interval inter_firstsubtree = m_first_subtree->tdomain() & t;
Interval inter_secondsubtree = m_second_subtree->tdomain() & t;

assert(inter_firstsubtree != inter_secondsubtree); // both degenerated

if(inter_firstsubtree.is_degenerated() && !inter_secondsubtree.is_degenerated())
return m_second_subtree->eval(inter_secondsubtree);
p = m_second_subtree->eval(inter_secondsubtree);

else if(inter_secondsubtree.is_degenerated() && !inter_firstsubtree.is_degenerated())
return m_first_subtree->eval(inter_firstsubtree);
p = m_first_subtree->eval(inter_firstsubtree);

else
{
pair<Interval,Interval> p_first = m_first_subtree->eval(inter_firstsubtree);
pair<Interval,Interval> p_second = m_second_subtree->eval(inter_secondsubtree);
return make_pair(p_first.first | p_second.first, p_first.second | p_second.second);
p = make_pair(p_first.first | p_second.first, p_first.second | p_second.second);
}
}

// Outside tdomain
if(t.lb() < tdomain().lb() || t.ub() > tdomain().ub())
{
p.first |= NEG_INFINITY;
p.second |= POS_INFINITY;
}

return p;
}

int TubeTreeSynthesis::time_to_index(double t) const
Expand Down

0 comments on commit bed28ab

Please sign in to comment.