Gracias Gracias:  0
Resultados 1 al 1 de 1

Tema: animation Temporal Verification

  1. #1
    Administrador y fundador. Avatar de 3dpoder
    Fecha de ingreso
    Apr 2002

    Animation Temporal Verification

    Animation Temporal Verification
    By Hamed Zaghaghi

    animation Temporal Verification-screenshot.jpg

    Temporal verifiers are mathematical tools that verify a temporal model against a temporal property, (i.e. properties that talque about time), and answer the question, “Does this temporal model satisfy these temporal propertiesí”.

    This concept is used by many researchers in the field of Software and Hardware Engineering, and I bring it to the world of computer animations.

    “Animation Temporal Verification” is a new and novel approach in computer graphics that lets us:

    • verify animations against temporal properties that can be extracted from story chek temporal constraints for animations
    • A temporal property is a temporal logic formula that will described later in this text. For example:

    Always (Cube1.LocX>=100.0)

    that means X part of Cube1 location should always be greater than or equal to 100.0.

    Here you can see some fundamental definitions for understanding what we can do with this tool to improve the time of checks and verifications.

    Linear Temporal Logic
    Linear temporal logic (LTL) is a modal temporal logic with modalities referring to time.

    LTL is built up from a set of propositional variables p1,p2,..., the usual logic connectives (not, and, or, implies) and the following temporal modal operators Next, Globally or Always, Eventually or Future, Until.

    An LTL formula can be evaluated over an infinite or finite sequence of truth evaluations and a position on that sequence. An LTL formula is satisfied by a sequence if and only if it is satisfied for position 0 on that sequence. The semantics for the modal operators is given as follows:

    • Next φ, holds at position i, if exists position i+1 and φ holds at position i+1
    • ψ Until φ, holds at position i if φ holds at some position j, and ψ has to hold at all positions in range [i to j).
    • Eventually φ or Future φ, holds at position i, if there was a position j>i and φ holds there. In other words Eventually φ holds if and only if True Until φ holds at position i.
    • Globally φ or Always φ, holds at position i if and only if Not Eventually Not φ holds at that position, in other words Globally φ holds at position i if φ holds at all positions.

    Important Properties:
    We can construct various temporal properties with linear temporal logic, but there are two main types of properties that can be expressed using this logic:

    • Safety properties (Globally Not φ): usually state that something bad never happens.
    • Liveness properties (Globally Eventually φ) or Globally(ψ Implies Eventually φ): state that something good keeps happening.

    See [1,2] for more information about temporal logic.

    This feature is implemented completely using Python and is available for Blender using the scripts menú after installation.

    You can get the Python script and it's required module, pycamc, from

    You can find more information about it's licence and how you can install it from above project page.

    How To Use It
    After installing it, open blender and open the script window in some area in blender. See Fig.1.

    animation Temporal Verification-fig1.jpg

    Then in the script window select the Animation Temporal Verification item from the Animation sub menú of the Script menú. See Fig. 2.

    animation Temporal Verification-fig2.jpg

    After opening the script you can see a form like the one in Fig. 3. and works as follows:

    animation Temporal Verification-fig3.jpg

    • Open/Save Buttons opens/sabes information from/to a file.
    • Temporal Constraint text box, should contain a temporal property
    • Start and End number boxes, shows start frame and frame of verification.
    • Verify button, starts verifying the Temporal Constraint
    • Add Proposition button adds new text boxes to the form so you can input a relational expression as a proposition there. See Fig. 4

    animation Temporal Verification-fig4.jpg

    • Name text box specifies the name of the proposition and can be used in a Temporal Constraint
    • Value text box specifies the boolean expression related to the proposition name
    • Del button, deletes the proposition in it's row

    Here we want to verify a simple temporal behaviour in an animation. The sample scene contains two Cubes, named Cube1 and Cube2, a Lamp and a Camera, see Fig. 5.

    animation Temporal Verification-fig5.jpg

    Now consider that we set up the scene so Cube1 moves in the X direction from lower values to higher values of X and Cube2 moves in the X direction too but from higher values to lower values of X. See Fig. 6 and Fig. 7.

    animation Temporal Verification-fig6.jpg

    animation Temporal Verification-fig7.jpg

    Furthermore, we want that the X part of the Cube1 location is smaller than or equal to 20 until the Cube2 X location reaches the Cube1 X location.

    After setting up the scene, creating IPOs etc. we want to chek that the above statements are true according to this scene. To do so:

    1.Add two propositions

    • proposition 'const1' with value 'Cube1.LocX<=20'
    • proposition 'const2' with value 'Cube1.LocX<=Cube2.LocX'

    2.Add the following constraint in Temporal Constraint text box

    • 'Const1 Until Const2'

    3.Press Verify button to start verification process.

    animation Temporal Verification-fig8.jpg

    Final Words!
    First I should thanque my co-worker, Babaque Salimi, who helps me in the theoretical side of work, and then thanks to you for reading this article.

    Please get it, test it, and report its bugs!

    To get download it from
    or get latest trunque source with
    bzr branch lp:camc
    To report
    report bugs here
    email me or
    1.Amir Pnueli. The temporal logic of programs. In FOCS, IEEE, 1977.

    By Hamed Zaghaghi

    Miniaturas adjuntadas Miniaturas adjuntadas animation Temporal Verification-screenshot.jpg   animation Temporal Verification-fig1.jpg   animation Temporal Verification-fig2.jpg   animation Temporal Verification-fig3.jpg  

    animation Temporal Verification-fig4.jpg   animation Temporal Verification-fig5.jpg   animation Temporal Verification-fig6.jpg   animation Temporal Verification-fig7.jpg  

    animation Temporal Verification-fig8.jpg  
    Si vas a subir un trabajo al foro, hazlo adjuntando la imagen, archivo, vídeo o lo que sea, no publicando enlaces de otros sitios.

    |Agradecer cuando alguien te ayuda es de ser agradecido|

Temas similares

  1. Temporal en Gijon
    Por acortes en el foro Todo menos Infografía
    Respuestas: 0
    Último mensaje: 05-03-2014, 20:20
  2. Sistema de coordenadas temporal
    Por carpo88 en el foro Modelado
    Respuestas: 0
    Último mensaje: 27-02-2014, 19:59
  3. Un adios temporal
    Por TheOutsider en el foro Todo menos Infografía
    Respuestas: 57
    Último mensaje: 12-08-2009, 16:19
  4. Vincular de forma temporal
    Por tipostupendo en el foro Animación y Rigging
    Respuestas: 1
    Último mensaje: 17-12-2008, 14:21
  5. Photoshop, archivo temporal
    Por dumdum en el foro Problemas con Programas
    Respuestas: 2
    Último mensaje: 12-01-2006, 20:31

Actualmente estos son sus permisos de publicación en el foro.

  • -No puedes crear nuevos temas al no estar registrado o no haber iniciado sesión en el foro.
  • -No puedes responder temas al no estar registrado o no haber iniciado sesión en el foro.
  • -No puedes subir archivos adjuntos al no estar registrado o no haber iniciado sesión en el foro.
  • -No puedes editar tus mensajes al no estar registrado o no haber iniciado sesión en el foro.