合金错误签名

1 回答

• 3

  你的主要问题是Huth / Ryan书的第二版似乎是在2004年出版的，并且使用（毫不奇怪）合金分析仪当时接受的语法，这也是（不出所料）不一样的 . 当前版本的Alloy Analyzer接受的语法 .

  因此，要在当前版本的分析器中运行它，您将必须了解（a）他们想要说的内容（b）他们试图说出的当时的Alloy语法，以及（c）当前的Alloy语法，足以将模型转换为当前语法 . （或者找到已经完成此操作的人 . ）幸运的是，Huth和Ryan详细解释了他们使用的Alloy语法，因此熟悉Alloy 4的人将模型转换为Alloy 4语法并不困难 .

  祝好运！

  [Postscript] 理论上你的任务的目标是让你熟悉Alloy Analyzer，而不是通过要求从旧的Alloy语法到新的Alloy语法的转换让你陷入深渊，我附加一个粗略的翻译将Huth / Ryan PDS模型转换为Alloy 4语法，并附带一些散布的注释 . （我说'rough'因为我没有花很多时间在上面，我可能已经错过了一些细微差别，特别是在谓词HighestVersionPolicy中，作者有点棘手 . ）如果你的任务的目标正是强迫你要通过语法丛林来战斗，只有你的本土聪明才能用作砍刀，然后我为搞乱这种经历而道歉 .

  在模块的顶部，主要的变化是调用排序库模块的方式 .

  module PDS
  
  open util/ordering[Number]
  

  在Component中，关键字'option'被当前关键字'lone'取代，我已经转录了一些Huth和Ryan的评论，试图帮助自己了解更好的情况 .

  sig Component {
      name: Name, // name of the component
      main: lone Service, // component may have a 'main' service
      export: set Service, // services the component exports
      import: set Service, // services the component imports
      version: Number  // version number of the component
  }{ 
     no import & export // imports and exports are disjoint 
                        // sets of services
  }
  

  在PDS的签名中，主要的变化是对基数语法的更改： ->? 变为 -> lone .

  // Package Dependency System
  // components is the set of Component in this PDS
  // schedule assigns to each component in the PDS
  //   and any of its import services 
  //   a component in the PDS that provides that service
  //   (see SoundPDSs, below)
  // requires expresses the component dependencies
  //   entailed by the schedule
  sig PDS {
      components: set Component,
      schedule: components -> Service ->  lone components,
        // any component / Service pair maps to at most
        // one component
      requires: components -> components
  }{ 
      // for every component in the system,
      // the services it imports are supplied (exported)
      // by some (other) component in the system
      components.import in components.export 
  }
  

  在SoundPDSs这一事实中，作者使用的是 with P 构造，我没有使用过 . 所以我把它拿出来，并且为了清晰起见重新表达了一些表达式，因为作者解释清晰度是他们使用 with P 结构的主要动机 . 确保你理解Alloy的盒子符号以及为什么P.schedule [c] [s]是另一种写c（.s.sdudule）[s]或s的方式（c . （P），这是值得的 . . 时间表）） .

  fact SoundPDSs {
    all P : PDS | {
      all c : P.components, s : Service |
        let c' = P.schedule[c][s] {
          (some c' iff s in c.import)
          // c and s require c' only iff c imports s
          &&
          (some c' => s in c'.export)
          // c and s require c' only if c' exports s
        }
      all c : P.components | P.requires[c]= P.schedule[c][Service] 
      // c requires precisely those components
      // that schedule says c depends on for some service
    }
  }
  
  sig Name, Number, Service {}
  

  从现在开始的重大变化是Huth和Ryan使用 fun 来定义各种属性，其中Alloy 4使用 pred - 关键字 fun 仍然是合法的，但它意味着一个函数（一个表达式在评估时返回一个值，不是布尔值而不是谓词 .

  pred AddComponent(P, P': PDS, c: Component)  {
      not c in P.components
      P'.components = P.components + c
  } run AddComponent for 3 but 2 PDS
  
  pred RemoveComponent(P, P' : PDS, c: Component) {
      c in P.components
      P'.components = P.components - c
  } run RemoveComponent for 3 but 2 PDS
  

  在HighestVersionPolicy中，我再次引入了框符号，试图使表达更清晰 . 请注意，此处未定义 prev - 它是模块顶部的导入指令（ open ... ）导入的关系之一，来自库模块以进行排序 .

  pred HighestVersionPolicy(P: PDS) {
      all s : Service, 
          c : P.components, 
          c' : P.schedule[c][s],
          c'' : P.components - c' {
              s in c''.export && c''.name = c'.name 
              => 
              c''.version in ^prev[c'.version]
          }
  } run HighestVersionPolicy for 3 but 1 PDS
  
  pred AGuideSimulation(P, P', P'' : PDS, c1, c2 : Component) {
      AddComponent[P, P', c1] 
      RemoveComponent[P, P'', c2]
      HighestVersionPolicy[P] 
      HighestVersionPolicy[P']    
      HighestVersionPolicy[P'']
  } run AGuideSimulation for 3
  
  assert AddingIsFunctionalForPDSs {
      all P, P', P'' : PDS, c : Component {
          AddComponent[P, P', c] && AddComponent[P, P'', c] 
          => P' = P''
      }
  }
  
  check AddingIsFunctionalForPDSs for 3
  

  version of their model given by Huth and Ryan on the web不包括他们在文中描述的StructurallyEqual谓词;我添加它以帮助确保我的模型的翻译工作 .

  pred StructurallyEqual(P, P' : PDS) {
    P.components = P'.components
    P.schedule = P'.schedule
    P.requires = P'.requires
  }
  
  run StructurallyEqual for 2
  

  同样地，它们不包括对AddingIsStructurallyFunctional的修复 - 意图可能是学生在Alloy中动态地执行它 .

  assert AddingIsStructurallyFunctionalForPDSs {
      all P, P', P'' : PDS, c : Component {
          AddComponent[P, P', c] && AddComponent[P, P'', c] 
          => 
          StructurallyEqual[P',P'']
      }
  }
  check AddingIsStructurallyFunctionalForPDSs for 3
  

  回复于 2024-05-05T09:45:25+08:00