modeling - Event-B, formal modelling : How to affect all the elements of a set to a relation -


i'm having quite lot of troubles event-b..

i'd make relation group of client client number each

i have relation of type :

cli(person) = nat1 (person finite set)

and in event have subset of person

where group <: person

and i'd affect cli relation i'd write intuitively : 

! x . x : group | cli(x) = numcli

am modelling right way? there method affectation i'd get?

i'm little bit guessing want achieve: cli maps person number:

variables   cli invariants   cli : person +-> nat1

you want event (let's call ev) assigns group of persons (called group) same number:

ev =   group, numcli   group <: person   numcli : nat1   cli := cli <+ (group**{numcli}) end

group ** {numcli} set of pairs (a relation) first element element of group , second numcli. operator <+ (relational override) removes elements cli first element if 1 of right operand , adds right operand. i.e. mappings of group in cli replaced or added mapping numcli.


Comments

Post a Comment

Popular posts from this blog

python - Installing PyDev in eclipse is failed -

unable read repository @ http://pydev.sf.net/updates/content.xml. sun.security.validator.validatorexception: pkix path building failed: sun.security.provider.certpath.suncertpathbuilderexception: unable find valid certification path requested target i installing pydev in eclipse using python, doesn't install successfully. gives above error. happened? how solve error? i had error when trying install on laptop behind corporate firewall. couldn't tell setup of firewall, not sure of root cause. i got passed error installing pydev eclipse when out behind firewall. another way got around have eclipse on non-firewalled machine, install pydev eclipse, , copy whole eclipse directory non-firewalled machine firewalled machine. there better way, , way fix properly, didn't have time work out firewall doing. this on windows 7 machine (yeah know) not work *nix versions installed through package manager yum or apt.
Read more

PHP OOP-based login system -

lets building oop-based user authentication system, , incorporate following principles: direct injection, inheritance, encapsulation, polymorphism , single responsibility principle. my background in programming has relied on procedural programming, , thus, finding difficult put these practices correct use. assume have these classes: class config { public function set($key, $value); public function get($key, $default = null); } class user { public function __construct(pdo $dbh, $id = null); public function setprofile(profile $profile); } class auth { public function __construct(config $config); public function login($username, $password, $keeploggedin = true); public function isloggedin(); public function getloggedinuser(); public function logout(); public function register(array $data); } class session { public function start($sessionname = null); public function write($key, $value); public function read($key, $default =...
Read more

python - Exception while importing pymorphy2 -

i've installed pymorphy2 using pip: requirement satisfied (use --upgrade upgrade): pymorphy2 in /usr/local/lib/python2.7/site-packages requirement satisfied (use --upgrade upgrade): docopt>=0.6 in /usr/local/lib/python2.7/site-packages (from pymorphy2) requirement satisfied (use --upgrade upgrade): pymorphy2-dicts<3.0,>=2.4 in /usr/local/lib/python2.7/site-packages (from pymorphy2) but when i'm trying import library in python interactive shell this: >>> import pymorphy2 traceback (most recent call last): file "<stdin>", line 1, in <module> file "/usr/local/lib/python2.7/site-packages/pymorphy2/__init__.py", line 3, in <module> .analyzer import morphanalyzer file "/usr/local/lib/python2.7/site-packages/pymorphy2/analyzer.py", line 10, in <module> pymorphy2 import opencorpora_dict file "/usr/local/lib/python2.7/site-packages/pymorphy2/opencorpora_dict/__init__.py", line 4, ...
Read more