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
    Mensajes
    15,455

    Animation Temporal Verification

    Animation Temporal Verification
    By Hamed Zaghaghi




    Introduction
    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.

    Definitions
    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.

    Syntax
    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.

    Semantic
    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.

    Implementation
    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 http://launchpad.net/camc.

    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 área in blender. See Fig.1.



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



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




    • 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




    • 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

    Example
    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.



    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.





    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.



    Final Words!
    First I should thank 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 https://launchpad.net/camc
    or get latest trunque source with
    bzr branch lp:camc
    To report
    report bugs here
    https://bugs.launchpad.net/camc/1.0/+bugs
    email me
    hamed.zaghaghi@gmail.com or zaghaghi@ut.ac.ir
    Refrencess
    1.Amir Pnueli. The temporal logic of programs. In FOCS, IEEE, 1977.
    2.http://en.wikipedia.org/wiki/Linear_temporal_logic.

    By Hamed Zaghaghi
    www.blenderart.org

    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. http://www.foro3d.com/f45/forma-correcta-de-insertar-imagenes-y-archivos-en-nuestro-mensaje-98930.html

    |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. archivo temporal en autocad
    Por dixan en el foro Diseño Gráfico y CAD
    Respuestas: 5
    Último mensaje: 12-03-2008, 21:54
  5. Duda Incapacidad Temporal
    Por devnul en el foro Todo menos Infografía
    Respuestas: 0
    Último mensaje: 27-10-2005, 02:17

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.
  •