Compass Gait in Acumen

Anita just got back from a three-week trip to the US, during which time she visited the Power Systems Lab at Portland State University, the MAHI Lab at Rice University, the Nuclear Robotics Group and the Human Centered Robotics Lab at the University of Texas at Austin, and the AMBER Lab at Texas A&M University.

During her visit to the AMBER Lab, Anita and Ryan Sinnet implemented a passive compass gait model in Acumen, and used the Acumen3D extension to generate a 3D animation. A screen shot of the animation and the corresponding Acumen code can be found below.

class Main(simulator)
  private
    q1=0; q2=0; q1'=-0.5; q2'=2; q1''=0; q2''=0; //theta1 and theta2 angles
    L=1; M=10; m=5; pi=3.1416; g=9.81; //model constants
    s=0.06; //slope of the surface
    pm1x=0; pm1z=0; pM2x=0; pM2z=0; pm3x=0; pm3z=0;
    p2z=0; p2x=0; //position of stance foot
    sfx=0; sfz=0; //position variable for animation
    h=0; h'=0; //guards

    _3D=[["Sphere",[0,0,0],0.01*5,[1,0,0],[0,0,0]],
         ["Sphere",[0,0,0],0.01*10,[1,0,0],[0,0,0]],
         ["Sphere",[0,0,0],0.01*5,[0,1,0],[0,0,0]],
         ["Cylinder",[0,0,-1/2],[0.01,1],[0,0,1],[3.1416/2,0,0]],
         ["Cylinder",[0,0,-1/2-1/2],[0.01,1],[0,0,1],[3.1416/2,0,0]],
         ["Box",[0,0,0],[10,2,2],[0.5,0.5,0],[3.1416/2,0.06,0]]];
  end

  //DINAMICS EQUATIONS
  //theta 1: angle between vertical and stance foot
  q1''[=](2*(2*q1'*q2'*L*m*sin(q2) + q2'^2*L*m*sin(q2) + q1'^2*L*m*(sin(q2) - sin(2*q2)) + g*(-2*(m + M)*sin(q1) + m*sin(q1 + 2*q2))))/(L*(-3*m - 4*M + 2*m*cos(2*q2)));

  //theta 2: angle between legs
  q2''[=](-2*(-2*q1'^2*L*(-3*m - 2*M + 2*m*cos(q2))*sin(q2) +      2*q1'*q2'*L*m*(sin(q2) - sin(2*q2)) + q2'^2*L*m*(sin(q2) - sin(2*q2)) +      g*(-2*(m + M)*sin(q1) + (3*m + 2*M)*sin(q1 - q2) - 2*m*sin(q1 + q2) -        2*M*sin(q1 + q2) + m*sin(q1 + 2*q2))))/   (L*(-3*m - 4*M + 2*m*cos(2*q2)));

  //ADDITIONAL EQUATIONS FOR ANIMATION
  //position of link 1 - middle of stance leg
  pm1x[=] -(L*sin(q1))/2;
  pm1z[=] (L*cos(q1))/2;

  //position of link 2 - hip joint
  pM2x[=]-L*sin(q1);
  pM2z[=]L*cos(q1);

  //position of link 3 - middle of swing leg
  pm3x[=](L*(-2*sin(q1) + sin(q1 + q2)))/2 ;
  pm3z[=]L*cos(q1) - (L*cos(q1 + q2))/2 ;

  //reference position of stance foot - just for animation
  p2x[=]L*(-sin(q1) + sin(q1 + q2));
  p2z[=]L*(cos(q1) - cos(q1 + q2));
 
   _3D[=][["Sphere",[sfx+pm1x-2,0,sfz+pm1z],0.01*m,[1,0,0],[0,0,0]],
         ["Sphere",[sfx+pM2x-2,0,sfz+pM2z],0.01*M,[1,0,0],[0,0,0]],
         ["Sphere",[sfx+pm3x-2,0,sfz+pm3z],0.01*m,[0,1,0],[0,0,0]],
         ["Cylinder",[sfx+pm1x-2,0,sfz+pm1z],[0.01,L],[0,0,1],[3.1416/2,q1,0]],
         ["Cylinder",[sfx+pm3x-2,0,sfz+pm3z],[0.01,L],[0,0,1],[3.1416/2,q1+q2,0]],
         ["Box",[0-2,0,0],[20,0.01,2],[0.5,0.5,0],[3.1416/2,-s,0]]];

  //GUARD
  h[=]2*L*(1/cos(s))*sin(q2/2)*sin(q1 + q2/2 + s);
  h'[=]2*(q1' + q2'/2)*L*cos(q1 + q2/2 + s)*(1/cos(s))*sin(q2/2) +  q2'*L*cos(q2/2)*(1/cos(s))*sin(q1 + q2/2 + s);

  if h <= 0  &&  h' < 0 && q2>0.05

    //RESET MAP
    //reset for dinamics equation
    q1=q1+q2;
    q2=-q2;
    q1'=(q2'*m + q1'*(m - 2*(m + 2*M)*cos(q2)))/(-3*m - 4*M + 2*m*cos(2*q2));
    q2'=(q2'*m*(-1 + 2*cos(q2)) + 8*q1'*(m + M)*(1 + 2*cos(q2))*sin(q2/2)^2)/   (-3*m - 4*M + 2*m*cos(2*q2));
   
    //just for animation
    sfx=sfx+p2x;
    sfz=sfz+p2z;

  end
end

Comparing Acumen to a framework for hybrid system verification

During the past week Adam has extended a report comparing Acumen to related work with the paper "Design principles for an extendable verification tool for hybrid systems" by Frehse and Ray. The paper describes a framework which bears some interesting similarities to Acumen. The framework provides APIs and components on which several semantics for a hybrid system model can coexist and share functionality. The emphasis in this framework is on verification, and example semantics (instances of the abstract framework APIs) based on Linear Hybrid Automata and Support Functions are given in the paper. Further, Adam has continued working on the virtual experimentation paper.

Simpler event handling

Last week Jan worked on improving the support for nonlinear invariants in Acumen's enclosure semantics and on alternative simulation time subdivision strategies. Michal and Jan also managed to simplify the event handling algorithm, by removing enclosures entirely from the event tree, so that it can be built up using vectors of intervals. The main benefit of this change, besides the simplification of the specification and implementation of event handling, is that the use of invariants to improve enclosures can now be easily described in terms of intersection of interval boxes. In the coming week Jan will make a formal analysis of the algorithm worked out for a simple example, and on a simplification of the solver algorithm specification.

Two papers and a library related to Acumen's enclosure semantics

During the past week Adam has been comparing the enclosure semantics of Acumen to three sets of algorithms that address the problem of reliability in simulations of hybrid systems. The first one, described in An asynchronous integration and event detection algorithm for simulating multi-agent hybrid systems by Esposito et. al. is an algorithm for simulating hierarchical, multi-rate, hybrid systems in which event detection is guaranteed and which makes it possible to simulate using a lower average integration rate. The second one, described in Robustness of Model-based Simulations by Fainekos et. al. is a method for statically analysing a concrete Simulink simulation in order to detect whether uncertainties in the inputs or parameters of the model, or computational errors, could have produced a result that differs from that of the given simulation. The analysis compares the sequence of Simulink blocks traversed by the simulation and warns the user if a different sequence is possible given the uncertainties present in the model, or due to floating point computation errors. The third set of algorithms is a MATLAB toolbox for validated numerical computation called INTLAB. It includes several data types and algorithms which are useful when building validated ODE IVP solvers like that of Acumen's enclosure semantics, including interval- and interval polynomial arithmetic, validated standard function approximations, integration of such functions as well as automatic differentiation. During the coming week Adam will focus on writing a survey of tools for virtual experimentation.

Computing mode invariant sets

Last week Jan worked on the enclosure interpreter, mainly focusing on additions that support more complex benchmarks. A modified version of the bouncing ball model, which tracks the energy of the ball as well as its position and velocity, has been the guiding example. The most demanding of the required additions is the computation of the support set of mode invariant predicates which comprise nontrivial numeric expressions. It is this set that allows the interpreter to use the mode invariant to reduce the over-approximation of the computed enclosures. Jan's idea was to enclosure-evaluate the expressions in the invariant and then use a simple interval constraint solving technique to compute a conservative approximation of the support. While this approach works well for linear expressions and for nonlinear expressions in one variable, mixed-variable nonlinear expressions lead to excessive over-approximation of the support. Jan suspects that this over-approximation may be one of the reasons why the benefits of adding the energy to the bouncing ball model could not be observed. Jan also spent some time experimenting with an alternative strategy for subdivision of the simulation time. In the coming week Jan will continue to work on the invariant support computation algorithm.

Studying at Rice

Yingfu has been studying at Rice for two months and just finished two mid-term exams last week.  The course "Principles of programming languages" taught by Cartwright is very interesting which not only focuses on building blocks, semantics and type systems of programming language but also introduces some fundamental concepts including alonzo church's lambda calculus back to 1930s.  And the projects are using Scala to write a small functional language called "Jam".  The course "System dynamics" taught by Marcia teaches yingfu some mechanical background starting with the classic mass-spring-damper systems.  The last course is  Algorithmic Robotics taught by Lydia, which introduces many algorithms for doing motion planning.