alloy

    0

    1答えて

    私は合金に慣れていないので、これはおそらく簡単な質問です。私はオンラインのチュートリアルを終わり、改訂版ソフトウェアアブストラクションを読んでいます。 r' = {b:B, a:A, c:C | a->b->c in r} テキストこれはB-> A-> Cの新しい関係を定義することを言う:34ページ、ページの下部にある例があります。私はr 'の明示的な順序がこのステートメントによってどのように

    0

    1答えて

    それは言う: をお手元にモデルに最適なものは何でもイディオム を使用して自由になるよう合金は、モデルのための固定のイディオムを持っていません。 本は、このようなチェックイン、チェックアウト、および入室などのイベントを伴うホテル事業を、モデル化するために「イベントイディオム」を使用しての偉大な例を示します。 "オブジェクト指向のイディオム"があると私は信じていますか?モデリングには他にどのようなイデ

    0

    1答えて

    矢印(製品)演算子を理解するために、私はWhitePagesのモデルを作成しました。各白いページには名前からアドレスへのマッピングがあります(この名前/アドレスマッピングは矢印演算子を使用します)。私は、白いページの名前/アドレスマッピングを示す述語を作成しましたw。私が指定した述語では、名前/アドレスの関連付けの数は3です。以下のモデルを参照してください。 矢印演算子の定義によれば、Name->

    0

    1答えて

    「天気」をRainy,Sunny,Cloudyのいずれかにします。 「天気」は、都市と天気の関係です。そのモデルを考える Boston – Sunny Seattle – Cloudy Miami – Sunny 、私は主張することができるはずです:: sig Forecast {weather: City -> one Weather} sig City, Weather {}

    1

    1答えて

    分析の効率を向上させるために(そしてここでは「アトム」に原子名が表示されるように)、順序関係が完全に固定されていると言われています(たとえば、enter link description hereまたは10やthereなど)自然な "順序)。 私が理解する限り、最適化はKodkod(in this piece of code)で行われます。しかし、記事や文書が詳細に説明されています(ブール行列の言

    0

    1答えて

    のs〜rは、ソフトウェア抽象の638ページのに相当します。私はs。〜rが〜(r。〜s)に等しいと信じていますは正しいステートメントです。

    0

    1答えて

    私はプロジェクトに取り組んでおり、ValloyとAlloyの両方でコード例を挙げていますが、Alloyスクリプトの構文が合金アナライザーによって認識されないという問題があります。 経験: fun Object::equals(obj: Object) { this.class = Object_Class => this..Object_equals(obj) this.class = Dim

    1

    1答えて

    私はプロジェクトを少し力強くしようとしていますので、私はadd関数を書くことに決めました。私は合金のウェブサイトにあるこの例からインスピレーションを得ました: pred add [b, b': Book, n: Name, t: Target] { b'.addr = b.addr + n->t } しかし、私がしたいのは、2つのオブジェクト "b"と "b '"(同じオブジェクト

    0

    1答えて

    合金が提供するユーティリティモジュールは、このウェブページに記載されています: http://alloy.mit.edu/alloy/documentation/quickguide/util.html しかし、それは、各モジュールによって提供される操作の一覧を表示しません。たとえば、Webページには発注モジュールがありますが、発注モジュールによってどのような操作が提供されているかはわかりません。