Animation temporal verification

[size=5]animation temporal verification[/size]
By hamed zaghaghi.




introduction
Temporal verifiers are mathematical tools that verify a temporal model against a temporal property, (i, 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 enginering, and i bring it todo 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 todo 100.0.
definitions
Here you can se some fundamental definitions for Understanding what we can do with this tool todo improve the time of checks and verifications.
linear temporal logic
Linear temporal logic (ltl) is a modal temporal logic with modalities referring todo 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 evalúated over an Infinite or finite sequence of truth evalúations 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, and ψ, has todo hold at all positions in range [i to).
  
• 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 god keps happening.

Se [1,2] for more información about temporal logic.
implementation
This característica is implemented completely using Python and is available for Blender using the scripts menú After installation.

You can get the Python script and it required module, pycamc, from [url]http://launchpad.net/camc[/url].

You can find more información about it licence and how you can install it from above Project page.
how todo use it
After installing it, open Blender and open the script window in some área in Blender. Se fig.1.



Then in the script window select the animation temporal verification item from the animation submenú of the script menú. Se fig. 2.



After opening the script you can se ha form like the one in fig. 3, and works as follows:

• open/save buttons opens/sabes información 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 todo the form so you can input a relational expression as a proposition there. Se fig. 4
  

• name text box specifies the name of the proposition and can be used in a temporal constraint.
  
• value text box specifies the bolean expression related todo the proposition name.
  
• del button, deletes the proposition in it row.
  

example
Here we want todo verify a simple temporal behaviour in an animation. The sample scene contains two cubes, named cube1 and Cube 2, a Lamp and a Camera, se fig. 5.



Now consider that we set up the scene so cube1 moves in the x direction from lower values todo higher values of x and Cube 2 moves in the x direction todo but from higher values todo lower values of x. Se fig. 6 and fig. 7.




Furthermore, we want that the x part of the cube1 location is smaller than or equal todo 20 until the Cube 2 x location reaches the cube1 x location.

After setting up the scene, creating Ipos etc. We want todo chek that the above statements are true according todo this scene. To do so:
1. Add two propositions.

• proposition const1 with value cube1. Locx<=20
  
• proposition const2 with value cube1. Locx<=Cube 2. Locx.
  

2. Add the following constraint in temporal constraint text box.

• const1 until const2
  

3. Press verify button todo 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 gracias todo you for reading this article.

Pléase 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.
[url]https://bugs, launchpad.net/camc/1.0/+bugs[/url]
Email me.
[email]hamed, zaghaghi@gmail.com[/email] or [email]zaghaghi@ut, (*.ac), ir[/email]
Refrencess.
1. Amir pnueli. The temporal logic of programs. In focs, explorer, 1977.
2.[url]http://en.wikipedia.org/wiki/linear_temporal_logic[/url].

By hamed zaghaghi.
[url]www.blenderart.org[/url].


-- IMÁGENES ADJUNTAS --