tulip-control-users — questions about using TuLiP; if you are unsure, ask here first!

Re: [tulip-control-users] Asking for help about TuLiP Toolbox

[Scott C. L. <sco...@gm...>]

The attachments to the original email were scrubbed before posting to
the mailing list, but I think that we can try to resolve the questions
before including bulk source code and output. I give responses in-line
below.

On 04/07/2017 11:39 PM, Yufei Huang wrote:
> Dear Scott,
> 
> My name is Yufei Huang and I am a graduate student in the University of
> Maryland. I am working for Dr. Huan Xu on a project which aims at using
> temporary logic planning to help a UAV avoid several obstacles. Thank you
> for your TuLiP toolbox but I meet some problems with it.
> 
> Currently I simplify the problem into only one obstacle and I devide a 3D
> space into a 3*3*3 cube(just like a Rubic cube).
> 
> I place the UAV in the middle of one surface and it wants to go to the
> middle of the opposite surface. Meanwhile, the obstacle is in the middle of
> the cube. And I am using the program which is named "discrete.py" in the
> examples trying to solve my problem.
> However, I don't know how to translate the specification, which
> is"[]<>(UAV<->destination) && [](UAV = !obstacle)". Also, I don't quite
> understand how to define the environment variables and the system
> variables.
> 

What is the interpretation of the following formula?

    UAV = !obstacle

In contrast, from the other subformula that you give,

    UAV <-> destination,

I guess that `UAV` and `destination` can take Boolean values TRUE and
FALSE, so that comparing them with `<->` is defined.

> When I remove the obstacle from the question, the result seems correct,
> which is in the attached file named "UAVtrans.png". However, I have trouble
> adding the obstacle into the system. The program, which is named
> "UAVtrans.py" in the attached files, always shows "Unrealizable". But I
> cannot tell where I made the mistake.
> 

The answer to my question above might help here.

> Could you please help me point out where I am wrong? And may I ask how to
> define the environment variables and the system variables?
> 
Can you be more detailed in your question about defining environment and
system variables? Did you try following the example discrete.py, which
includes both env and sys variables?

Re: [tulip-control-users] Writing specs in TuLip

[Scott C. L. <sco...@gm...>]

On 04/28/2017 02:23 PM, Andreas Jacob wrote:
> Hi,
> 
> 
> I'm new with using TuLiP and facing great difficulty with entering gr1 specs into the tool. All examples provided are based on the same robot scenario, so I cannot grasp how to work with different ltl operators. Do you have any suggestions to look at any other examples that might help me with representing GR1 into TuLiP?
> 

In the TuLiP sourcetree, a somewhat nontrivial example is
examples/developer/fuel_tank/double_tank.py

In the docstring of the file double_tank.py, you will find alternative
values of parameters to make the problem instance easier to solve, e.g.,
allowing a smaller abstraction to be constructed.

> 
> In particular, I have been working with a very small and simple example but unfortunately can't successfully enter into TuLiP. Please see Section 3.1.6 (Specification Example) from Clemens Wiltsche Masters theses: https://arxiv.org/pdf/1304.6898.pdf. Any leads/suggestions on working with this small example in TuLiP would be very much appreciated. Thanks a lot for your time.
> 
> 

Are you interested in formulae of the form

    [](x -> <>y)

as given near the beginning of Section 3.1.6? The function
response_to_gr1() in tulip.spec.gr1_fragment translates such formulae
into an appropriate GR(1) format. Note that the translation introduces
an auxiliary variable, `aux`. E.g., below is an example where x is an
environment variable and where x is assumed to be TRUE repeatedly. Note
that y can be assigned TRUE arbitrarily because it is not constrained.

import tulip.spec.gr1_fragment
import tulip.synth
spc = tulip.spec.gr1_fragment.response_to_gr1('x', 'y')
del spc.sys_vars['x']
spc.env_vars = {'x': 'boolean'}
spc.env_prog = {'x'}
spc.sys_init = ['!x && !y && !aux']
spc.qinit = '\E \E'
print(spc.pretty())
strategy = tulip.synth.synthesize(spc)
print(strategy)

[tulip-control-users] Writing specs in TuLip

[Andreas J. <and...@ou...>]

Hi,


I'm new with using TuLiP and facing great difficulty with entering gr1 specs into the tool. All examples provided are based on the same robot scenario, so I cannot grasp how to work with different ltl operators. Do you have any suggestions to look at any other examples that might help me with representing GR1 into TuLiP?


In particular, I have been working with a very small and simple example but unfortunately can't successfully enter into TuLiP. Please see Section 3.1.6 (Specification Example) from Clemens Wiltsche Masters theses: https://arxiv.org/pdf/1304.6898.pdf. Any leads/suggestions on working with this small example in TuLiP would be very much appreciated. Thanks a lot for your time.


Sincerely,

Andreas
-------------- next part --------------
An HTML attachment was scrubbed...

[tulip-control-users] Fwd: Asking for help about TuLiP Toolbox

[Scott C. L. <sco...@gm...>]

-------- Forwarded Message --------
Subject: Asking for help about TuLiP Toolbox
Date: Fri, 7 Apr 2017 23:39:04 -0400
From: Yufei Huang <...>

Dear Scott,

My name is Yufei Huang and I am a graduate student in the University of
Maryland. I am working for Dr. Huan Xu on a project which aims at using
temporary logic planning to help a UAV avoid several obstacles. Thank
you for your TuLiP toolbox but I meet some problems with it.

Currently I simplify the problem into only one obstacle and I devide a
3D space into a 3*3*3 cube(just like a Rubic cube).

I place the UAV in the middle of one surface and it wants to go to the
middle of the opposite surface. Meanwhile, the obstacle is in the middle
of the cube. And I am using the program which is named "discrete.py" in
the examples trying to solve my problem.
However, I don't know how to translate the specification, which
is"[]<>(UAV<->destination) && [](UAV = !obstacle)". Also, I don't quite
understand how to define the environment variables and the system variables.

When I remove the obstacle from the question, the result seems correct,
which is in the attached file named "UAVtrans.png". However, I have
trouble adding the obstacle into the system. The program, which is named
"UAVtrans.py" in the attached files, always shows "Unrealizable". But I
cannot tell where I made the mistake.

Could you please help me point out where I am wrong? And may I ask how
to define the environment variables and the system variables?

Thank you so much!

Yufei Huang

-------------- next part --------------
A non-text attachment was scrubbed...
Name: UAVtrans.png
Type: image/png
Size: 43297 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: UAVtrans.py
Type: application/octet-stream
Size: 5508 bytes
Desc: not available