問題タブ [event-b]

event-b のラムダ式を1 つだけ使用して素数のシーケンスを生成できるかどうか疑問に思います。これは私がこれまでに持っているものです:

@axm1素数のセットを生成し@axm2、シーケンスのタイプを定義し、@axm3このセットをさらに決定論的な解に制約します。1つのラムダ式でこれを行う方法がわかりません。それが可能だとは思いませんが、他の人の考えを知りたいです。

次のような質問があります。

小学校のクラスには、多くの子供とさまざまな本が含まれています。子供たちが読んだ本を追跡するモデルを書きます。子供と本の間の関係を維持する必要があります。

だから私は自分の文脈を持っています

そして、私のマシンは次のとおりです。

readBooks ∈ students → ℕ はエラーを起こしています。明らかに、私はこれを間違ってモデリングしています。これで私を助けることができる体はありますか？イベント B は初めてで、どうすればよいか本当にわかりません

私はイベント B の初心者であり、セット PERSONNE にセット RESIDENT を含むセット CLIENT が含まれるマシンをモデル化しようとしています... ロダンのドキュメントを検索しましたが、何も見つかりませんでした.. . コンテキストは次のとおりです

そして、これがマシンです

アイデアはあると思いますが、取得したさまざまなエラーを解決する方法を管理できません: タイプ CLIENT と PERSONNE が一致しません (3 回) タイプ RESIDENT と CLIENT が一致しません (2 回)...

私はEvent-Bでかなり多くの問題を抱えています..

クライアントのグループからクライアント番号ごとに関係を作りたい

私はそのタイプの関係を持っています:

cli(PERSON) = NAT1 (人は有限集合)

イベントでは、人のサブセットがあります

そして、私が直感的に書くものをcli関係に影響を与えたいと思います:

私はそれを正しい方法でモデリングしていますか？私が得たい愛情を得る方法はありますか？

いくつかの条件が与えられたとき、変数の次の状態が何らかの命題に当てはまることを確認したいと思います。私はロダンが認めたものを作ることができませんでした。

私の正確なケースは、次の不変条件です。doorロックがオンのときに変数が変更されないようにしたい。変数doorは、OpenまたはClosed

これPrimaryLockはOn、次にどのイベントがトリガーされても、ドアの状態が変わらないことを意味します。

これは Event-b を使用して可能ですか、それとも変数を追加して問題を解決する必要がありますか?

ProBで多数のコードを視覚化する際に問題があります。このグラフは、ProB の (Graphviz の dotty を使用して) サーバーのログイン セクションを示していますが、グラフを取得するための多数のコードに対する解決策はありません。あなたの提案やアイデアを教えてください。

最新バージョンの Rodin Platform に完全に洗練されたモデルをインポートしました。このプロジェクトでは、ProB アニメーターで IUMLB を使用しようとしています。しかし、プロジェクトには既に構成済みの AnimB アニメーターがあり、最新の Rodin Software ではサポートされていません。エラーには、「不明な構成 org.animb.valuation.valBase」と記載されています。

この AnimB 構成をプロジェクトから削除または修正するにはどうすればよいですか?