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:
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.
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 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 area 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
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
3.Press Verify button to start verification process.
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 https://launchpad.net/camc
or get latest trunque source with
bzr branch lp:camc
report bugs here
1.Amir Pnueli. The temporal logic of programs. In FOCS, IEEE, 1977.
By Hamed Zaghaghi