alloy - Unexpected results in playing with relations - 


/* sig { }  sig b { } */  pred rel_test(r : univ -> univ) {     # r = 1 }  run {     r : univ -> univ {         rel_test [r]     } } 2

running small test, $r contains 1 element in every generated instance. when sig a , sig b uncommented, however, first instance this:

enter image description here

in explanation, $r has 9 tuples here , still, predicate asks 1 tuple relation succeeds. wrong?

an auxiliary question: these 2 declarations equivalent?

pred rel_test(r : univ -> univ) pred rel_test(r : set univ -> univ)

the problem forbid overflow option set no integer semantics in alloy wrap around, , default scope of 3 (bits), indeed 9=1, can confirm in evaluator.

with signatures , b commented biggest relation can generated scope 2 has 4 tuples (since max size of univ 2), problem not occur.

it not occur in latest build because believe comes forbid overflow option set yes default, , option semantics of integers rules out instances overflows occur, precisely case when compute size of relation 9 tuples. more details alternative integer semantics can found in paper "preventing arithmetic overflows in alloy" aleksandar milicevic , daniel jackson.


Comments

Post a Comment

Popular posts from this blog

php - Wordpress website dashboard page or post editor content is not showing but front end data is showing properly -

Image
recently have uploaded wordpress site onto server. have uploaded wordpress site in sub-folder under root folder ../root(domain root folder)/wordpress (where host wordpress folder). now problem content data in page or post in dashboard of wordpress admin panel not showing - see image. but data showing in front view - see image. if not browser cache issue , not issue happened tinymce editor during upgrade; try add config file: define('concatenate_scripts', false);
Read more

javascript - Get parameter of GET request -

i make request: createxhrrequest( "get", fileurl, function( err, response ) { if( err ) { alert( "error get!" ); } alert(response); }); and full response: { "status" : "ok", "message" : "jvberi0xljqkjdduxdgkmy how can jvberi0xlj ? i try response.message , response["message"]. nothing works. just simple access this: var json = json.parse(response); json.message
Read more

javascript - Twitter Bootstrap - how to add some more margin between tooltip popup and element -

Image
i have not tryed since can't understand space between tooltip , element made/added bootstrap, tooltip near element triggers tooltip event. i make tooltip opening little bit away element, add more margin tooltip , eleemnt mean. i understand how in css if possible , if possible make both right,left,top,bottom tooltips hope question clear. this how tooltips looks on app: and , how should looks after this default css tooltip on top : .tooltip.top { padding: 5px 0; margin-top: -3px; } you can override in own css : .tooltip.top { margin-top: -10px; } note code work work tooltip on top, you'll nedd adapt css 3 other orientations : .tooltip.top { margin-top: -10px; } .tooltip.right { margin-left: 10px; } .tooltip.bottom { margin-top: 10px; } .tooltip.left { margin-left: -10px; }
Read more