search

BerkeleyLearnVerify / VerifAI

VerifAI is a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components.
BSD 3-Clause "New" or "Revised" License
170 stars 47 forks source link

Simple example #4

Closed TomyYamy closed 2 years ago

TomyYamy commented 5 years ago

I have made a very simple example by using /user/local/Webots/projects/languages/python/worlds/example.wbt at simpleExample branch. I checked it on Python3.6 & Webots 2018 & ubuntu18.04

TomyYamy commented 5 years ago

/VerifAI/examples/webots/controllers/verifai_supervisor$ python verifai_falsifier.py

It seems to work, but slightly there is small. Could you confirm why I have "Unsafe samples: Error table, Empty DataFrame" in the result?

Initialized sampler
Sample no:  0 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.14440970384343377, -0.04315398773646234), ROBOT2pos=(0.11410159605923209, 0.5798954706390909), ROBOT3pos=(0.10950036176882261, 0.3797367954768317))) 
Rho:  0.2071095021291585
Sample no:  1 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.11739403303024543, 0.0835915728307225), ROBOT2pos=(0.3181808107828712, 0.5238310464611365), ROBOT3pos=(-0.08673965617761942, 0.3071785242390448))) 
Rho:  0.20146853897439795
Sample no:  2 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(0.07053076424417903, 0.05807474007010904), ROBOT2pos=(0.6812931901685542, 0.5261802445125658), ROBOT3pos=(-0.2818569302974274, -0.2353283980180083))) 
Rho:  0.4408125077884049
Sample no:  3 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.6010818438981683, -0.435525079691919), ROBOT2pos=(0.3568563063988902, 0.42866855503097445), ROBOT3pos=(-0.24666893026970158, 0.1576750959493367))) 
Rho:  0.5298189061821029
Sample no:  4 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.194565900306383, -0.06848156133776084), ROBOT2pos=(0.41525163846211854, 0.2410731835218464), ROBOT3pos=(-0.13323256090541735, -0.0857984482985894))) 
Rho:  0.07612876091535602
Sample no:  5 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.4922153024778958, -0.2459867760380342), ROBOT2pos=(0.37552886478496406, 0.6870230716430303), ROBOT3pos=(-0.1871778439102529, 0.22035226746948322))) 
Rho:  0.5298189061821029
Sample no:  6 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.3342832797705116, -0.09134108479081937), ROBOT2pos=(0.007356523101056708, 0.6982477015723718), ROBOT3pos=(0.34631551010985717, 0.1013054218723044))) 
Rho:  0.5298189061821029
Sample no:  7 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.36444802716699576, -0.21831289100405304), ROBOT2pos=(0.1870501546547714, 0.5149629519195694), ROBOT3pos=(0.19062361549772688, -0.17593321531564454))) 
Rho:  0.5298189061821029
Sample no:  8 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.48754218585028913, -0.21177344029537765), ROBOT2pos=(-0.07704619735059907, 0.7742999117223489), ROBOT3pos=(0.3915961179223397, 0.11017183040800205))) 
Rho:  0.5298189061821029
Sample no:  9 
Sample:  SpacePoint(control_params=StructPoint(ROBOT1pos=(-0.537519269904413, -0.42754986090474606), ROBOT2pos=(0.6705972794555504, 0.5813058867656078), ROBOT3pos=(0.07504339547528716, 0.0639469725848067))) 
Rho:  0.5298189061821029
Unsafe samples: Error table
Empty DataFrame
Columns: [point.control_params.ROBOT1pos[0], point.control_params.ROBOT1pos[1], point.control_params.ROBOT2pos[0], point.control_params.ROBOT2pos[1], point.control_params.ROBOT3pos[0], point.control_params.ROBOT3pos[1]]
Index: []
TomyYamy commented 5 years ago

I think I need to clean up and try to be closed to be you guys coding style.

TomyYamy commented 5 years ago

Sorry I find "Unsafe samples: Error table, Empty DataFrame" comes from last code of verifai_falsifier.py

print("Unsafe samples: Error table")
print(falsifier.error_table.table)

In any case, I wonder if you could check that works correctly.

shromonag commented 5 years ago

Hi,

Thank you for your email. :)

The reason you are getting the error is because there are no counterexamples. Notice all the samples have positive rho, and hence safe. The empty data frame implies that there are no counterexamples and hence the table is empty.

Best, Shromona

On Wed, May 8, 2019 at 11:58 AM TomyYamy notifications@github.com wrote:

Sorry I find "Unsafe samples: Error table, Empty DataFrame" comes from last code of verifai_falsifier.py

print("Unsafe samples: Error table") print(falsifier.error_table.table)

In any case, I wonder if you could check that works correctly.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/BerkeleyLearnVerify/VerifAI/pull/4#issuecomment-490609026, or mute the thread https://github.com/notifications/unsubscribe-auth/ADIEAVSHY3OMQPYYQU7LZPDPUMPDRANCNFSM4HLS6N7Q .

TomyYamy commented 5 years ago

So now it works well. so I'll clean up the code from now.

TomyYamy commented 5 years ago

Applying SCENIC itself OK.

However I think we had better to split example also as a unit testing. Too much integrated example is difficult to understand user at first time.

How about implementing Webot+Falsifcation(=sample input+STL), Webot+Falsification(=sample SENIC+STL) separately?

shromonag commented 5 years ago

Hi,

Webot+Falsifications (no scenic) is already available in the cones_lanechange_supervisor

In the present release, scenic is used for scene generation only. We are now currently hooking that up to the falsifier loop and will let you know when it’s available.

Best, Shromona

On Thu, May 9, 2019 at 12:19 PM TomyYamy notifications@github.com wrote:

Applying SCENIC itself OK.

However I think we had better to split example also as a unit testing. Too much integrated example is difficult to understand user at first time.

How about implementing Webot+Falsifcation(=sample input+STL), Webot+Falsifcation(=sample SENIC+STL)?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/BerkeleyLearnVerify/VerifAI/pull/4#issuecomment-491032231, or mute the thread https://github.com/notifications/unsubscribe-auth/ADIEAVWM4Q7FEWXP2XIT7ATPUR2MZANCNFSM4HLS6N7Q .

TomyYamy commented 5 years ago

Yes, cones_lanechange_supervisor is Webot+Falsifications (no scenic) . but little bit complex as a1st step because it needs setting up tensorflow, opencv and PIL. Sometimes user fail to setup those (mainly tensorflow...).

In other word, cones_lanechange_supervisor = Webot(=Webot+tensorflow) + Falsifcation(=sample input+STL), and my suggestion is simple example = Webot + Falsifcation(=sample input+STL).

TomyYamy commented 5 years ago

SCENIC implementation is interesting.

So you means, previously SCENIC worked as a sampler or optimizer class, now your are trying to run at the insides of as a model or target side. I think good idea.

In addition, We suffered setting of pre-condition constraint and sometimes preconditions become complex and difficult to find SAT case of those. I request precondition class which handles and contains formula or model for that.

shromonag commented 5 years ago

I see, I do have an example like that, I can push it for you :)

On Thu, May 9, 2019 at 4:50 PM TomyYamy notifications@github.com wrote:

Yes, cones_lanechange_supervisor is Webot+Falsifications (no scenic) . but little bit complex to 1st step because it needs setting up tensorflow, opencv and PIL. Sometimes user fail to setup those (mainly tensorflow...).

In other word, cones_lanechange_supervisor = Webot(=Webot+tensorflow) + Falsifcation(=sample input+STL), and my suggestion is simple example = Webot + Falsifcation(=sample input+STL).

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/BerkeleyLearnVerify/VerifAI/pull/4#issuecomment-491106153, or mute the thread https://github.com/notifications/unsubscribe-auth/ADIEAVQCOLFWEP2YMD5QO53PUS2FZANCNFSM4HLS6N7Q .

TomyYamy commented 5 years ago

That's good! Thank you.