Polymorphic empty relation in Alloy? -

-

i run alloy command involves finding witnesses existentials, one:

pred foo {    x, y : e -> e |      baz[x,y] || qux[x,y]  }

alloy comes model foo true. @ model in visualizer, , find y happens empty relation. want dig deeper model , see whether baz or qux true. fire evaluator window , type baz[$foo_x, ???]. can type ???? since y empty, there no variable name $foo_y. , typing none or {} gives type-checking error.

does alloy provide empty relation can used @ type? or there way @ y witness though it's empty?

i belive baz[$foo_x, none->none] should work. relation none has arity 1, , using cross product can empty relations of desired arity. explanation can found in paper "a type system object models" jonathan edwards, daniel jackson , emina torlak.


Comments

Post a Comment

Popular posts from this blog

SVG stroke-linecap doesn't work for circles in Firefox? -

-
i've got problem svg stroke-linecap attribute. i've got circular progress bar in angularjs , set outer circle (blue one) have rounded "ends". @ fiddle . <svg ... height="130" width="130"> <!-- ngif: background --> <circle ... ng-if="background" fill="#fff" class="ng-scope" stroke-width="13" stroke="#cc3399" r="57.5" cy="65" cx="65" stroke-linecap="round" /> <!-- end ngif: background --> <circle ... fill="none" stroke-dashoffset="36.12831551628261" stroke-dasharray="361.28315516282623" stroke-width="13" stroke="#432db3" stroke-linecap="round" r="57.5" cy="65" cx="65" transform="rotate(-89.9, 65, 65)" /> </svg> how can that? ...
Read more

routes - Laravel 4 Wildcard Routing to Different Controllers -

-
realizing i'm going take beating this, have several questions "best practices" when constructing laravel route. do laravel routes run "first come first serve" top bottom? if route found, pass control controller (or perform action) , terminate? i have part of application acts url shortner. so, route looks this: route::get('/{id}', array('as' => 'home.text', 'uses' => 'homecontroller@text'), function($id){ //make sure id exists before pushing controller. if (storage::where('shortcode','=', $id)->count() > 0) { // route found } }); how can improved? one, i'm not sure how pass processing on controller conditionally.. sort of controller::make() ..? 3) there better way in laravel check if record exists versus doing mode::where('column','=','value')->count() 4) have legacy urls http://url.com/?...
Read more

cross browser - XSLT namespace-alias Not Working in Firefox or Chrome -

-
i transforming xhtml xhtml, need xslt stylesheet part of resulting document (the stylesheet contained in <script type"text/template"> element. using the xsl:namespace-alias instruction, works fine in ie, fails in both chrome , firefox. here relevant code: <xsl:output doctype-system="about:legacy-compat" omit-xml-declaration="yes" indent="yes" method="html" media-type="application/xhml" encoding="utf-8"/> <xsl:namespace-alias stylesheet-prefix="wxsl" result-prefix="xsl" /> <xsl:template match="head"> <!-- code omitted clarity --> <script type="text/template"> <wxsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/xsl/transform" xmlns="http://www.w3.org/1999/xhtml" xmlns:xhtml="http://www.w3.org/1999/xhtml" xmlns:eli="local"> ...
Read more