The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]

Microsoft Research выпустил версию TLA Toolbox для Linux

22.01.2010 20:31

Исследовательское подразделение Microsoft Research выпустило Linux версию интегрированной среды разработки для написания и проверки TLA+ (Temporal Logic of Actions) спецификаций, базирующихся на элементах темпоральной логики.

  1. Главная ссылка к новости (http://research.microsoft.com/...)
Автор новости: Трухин_Юрий_Владимирович
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/25118-microsoft
Ключевые слова: microsoft, linux, tla
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (22) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, NoName (?), 21:04, 22/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +9 +/
    И где это применимо?
     
     
  • 2.65, XoRe (ok), 12:46, 23/01/2010 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >И где это применимо?

    +1

    Кто-нибудь использовал?

     
  • 2.71, hhg (ok), 19:23, 23/01/2010 [^] [^^] [^^^] [ответить]  
  • +3 +/
    применимо таргонами в темпоральной зоне где-то на пути к Ракксле
     

  • 1.3, Аноним (-), 21:16, 22/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +6 +/
    o_O Не ожидал такого от них
     
  • 1.5, anonymous (??), 21:24, 22/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +5 +/
    Оо, давно ждал темпаральную логику, а типерь и под Линукс!! Пошёл ставить/где ебилды, etc.
     
     
     
    Часть нити удалена модератором

  • 3.15, JL2001 (ok), 22:27, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +4 +/
    >ну да, это ее исследовательское подразделение, так сказать ее часть

    тулсы вобще вроде на жаве написаны

     
  • 3.73, dq0s4y71 (ok), 18:50, 24/01/2010 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Лучшая половина? :)
     

  • 1.10, Аноним (-), 21:44, 22/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +7 +/
    Мельком прочёл лицензию - вроде никаких ловушек. Даже и не верится в такое от компании, в названии которой наличествует слово "Microsoft"
     
     
  • 2.11, Zenitur (?), 21:48, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +6 +/
    В новости про GCC также писали, что какие-то майкрософтские алгоритмы были включены в GCC. M-PETS кажется.
     
     
  • 3.17, User294 (ok), 22:29, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +7 +/
    А они потом с своим патентным троллингом не выплюнутся, как обычно?
     
     
  • 4.25, Zenitur (?), 23:12, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +6 +/
    >А они потом с своим патентным троллингом не выплюнутся, как обычно?

    Ой, да слухи всё это, про якобы нарушенные в ядре линукса 300 патентов... Агрессия со стороны Майкрософта. А где, эти нарушенные 300 парентов? Предъявите так сказать? А нету. А если предъявите, например, нарушенный патентик в коде управления памятью - да у нас есть 10 вариантов этого кода, которые под патент не подпадают! Изменим! Также и с GCC и M-PEC, будете рэкетировать - уберём, нафик нужно.

     
     
  • 5.72, User294 (ok), 00:30, 24/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    >Ой, да слухи всё это, про якобы нарушенные в ядре линукса 300
    >патентов... Агрессия со стороны Майкрософта.

    Знаете, на форуме языком пиндеть - это одно. А вот если  вы контора которая на мушке патентных троллей например - вот тут вы по другому ощущать это будете. И, собственно, у MS юристов много и если что-то есть - они вздуют по самые помидоры. Поэтому чем дальше от MSовских технологий, тем целее шкура, имхо. А что помешает MS специально вдувать технологии с целью потом нажиться? С фатами всякими примерно так и получилось - сперва дали всем подсесть а потом заявили - гоните бабки, а не то... Ну и где гарантии что с остальными их технологиями не выйдет точно такая же история? А если платить - так это из нашего с вами кармана в конечном итоге вынут. Ну а из чьего же еще? :)

     
  • 2.12, Аноним (12), 21:51, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +8 +/
    какая там лицензия?у меня не работает ссылка
     
     
  • 3.32, pavlinux (ok), 23:30, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +4 +/
    Unless otherwise indicated, the TLA Toolbox is made available by Microsoft Corporation
    under the terms and conditions of the Microsoft Research License Agreement provided
    below.
    The Compaq Corporation license below governs some of the code located
    in subdirectories tla2sany, tla2tex, tlc2, and util of the file tla2tools.jar.


      

     

  • 1.22, pavlinux (ok), 23:01, 22/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +5 +/
    У амерекосского бизнеса есть закон - Надо создать проблему, что бы продавать товар её решающий.
    (собственно, этот закон они тоже спиз...ли у Макиавелли, тот у Тита Ливия)



    Until ( !x ) {
           Future (x) {
                  Next( x ) {
                    All (x++);
                  }
    }   }

    тоже самое

    while ( !x ) { /* Until */
          if ( ++x )  { /* Future */
              
            if (x++) { /* Next */
                      do {
                          ....                  
                     } while (x++ ) /* All */
            }

        }
    }


    Ну и накой хрен эта темпоральная логика...
    Назад к ПРОЛОГУ и компьютеру Минск с троичной системой...

     
     
  • 2.28, Аноним (-), 23:19, 22/01/2010 [^] [^^] [^^^] [ответить]  
  • +2 +/
    compose в помощь. Если уж совсем припечёт, то вынесут на тулбокс или захоткеят наконец
     
  • 2.74, fr0ster (ok), 08:59, 25/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    ИМХО для построения той же диаграммы Ганта эту логику и использовать.
    Что же до Пролога, то на нем японцы уже собирались строить компы следующего поколения(и чем их Минск не устраивал? продали бы ведь), сейчас я только про одно использование пролога слышал, у нокии кажется для управления питанием в телефоне.
     
  • 2.76, Basiley (ok), 23:23, 25/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    почему "назад" ?
    пролог/эрланг - фьюче.
     

  • 1.75, ACCA (ok), 22:08, 25/01/2010 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Как всегда - PSL ниасилили, изобрели очередную инновацию. Походу планировали вылезти на рынок FPGA и железа вообще, но Windows Mobile - это уже репутация.

    Пора бы уже привыкать - слово Microsoft отгоняет клиентов, которые умеют хотя бы читать.

     
     
  • 2.77, fr0ster (ok), 08:50, 26/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    >Как всегда - PSL ниасилили, изобрели очередную инновацию. Походу планировали вылезти на
    >рынок FPGA и железа вообще, но Windows Mobile - это уже
    >репутация.

    А как связано TLA и FPGA?


    >Пора бы уже привыкать - слово Microsoft отгоняет клиентов, которые умеют хотя
    >бы читать.

    Это наблюдения или мечтания? Нормальный клиент не смотрит на названия а берет калькулятор и считает стоимость владения / использования. Если у решения на Винде будет стоимость меньше, выберет Винду, если на Линуксе - Линукс, и тд. Только стоимость эту подсчитать бывает сложновато.

     
     
  • 3.78, ACCA (ok), 09:35, 26/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    >>Как всегда - PSL ниасилили, изобрели очередную инновацию. Походу планировали вылезти на
    >>рынок FPGA и железа вообще, но Windows Mobile - это уже
    >>репутация.
    >
    >А как связано TLA и FPGA?

    Через PSL. Задайся вопросом - нахрена вообще нужен TLA?


    >>Пора бы уже привыкать - слово Microsoft отгоняет клиентов, которые умеют хотя
    >>бы читать.

    [...]
    >Винде будет стоимость меньше, выберет Винду, если на Линуксе - Линукс,
    >и тд. Только стоимость эту подсчитать бывает сложновато.

    Вот-вот. Появляется несколько неопределённых переменных, которые принимают на веру. По техническим параметрам маркетоиды слили вчистую, пробуют играть в TCO.

    Теперь посчитаем TCO для London Stock Exchange.
        1. Лицензия торговой площадки от M$
        2. Внедрение от M$
        3. Потери от слётов системы
        4. Покупка конторы с софтом для площадки под Linux
        5. Внедрение и перестройка торговой системы

    И сильно помог им калькулятор стоимости владения/использования?

    Ещё про стоимость владения/использования - про конторы, влетевшие на серьёзные бабки из-за виндовых троянов: http://voices.washingtonpost.com/securityfix/2009/10/avoid_windows_malware_ba

    "Не используйте Microsoft Windows для доступа к банковским счетам онлайн.
    [...]
    ...наиболее дешёвый и надёжный способ [для безопасной работы с финансами] - использовать read-only операционную систему, такую как Knoppix или Ubuntu [LiveCD]..."

     
     
  • 4.79, fr0ster (ok), 10:28, 26/01/2010 [^] [^^] [^^^] [ответить]  
  • +/
    >>>Как всегда - PSL ниасилили, изобрели очередную инновацию. Походу планировали вылезти на
    >>>рынок FPGA и железа вообще, но Windows Mobile - это уже
    >>>репутация.
    >>
    >>А как связано TLA и FPGA?
    >
    >Через PSL. Задайся вопросом - нахрена вообще нужен TLA?
    >

    Мало ли в ОпенСорсе велосипедов? С другой стороны а зачем диаграмма Ганта?
    Да и мне казалось, что FPGA узко связано с железом, а TLA более широко применяеть можно, как и PLS вроде как.

    >[оверквотинг удален]
    >>>Пора бы уже привыкать - слово Microsoft отгоняет клиентов, которые умеют хотя
    >>>бы читать.
    >
    >[...]
    >>Винде будет стоимость меньше, выберет Винду, если на Линуксе - Линукс,
    >>и тд. Только стоимость эту подсчитать бывает сложновато.
    >
    >Вот-вот. Появляется несколько неопределённых переменных, которые принимают на веру. По техническим параметрам
    >маркетоиды слили вчистую, пробуют играть в TCO.
    >

    Считали не так. Да и маркетоиды тут не к месту, речь идет о людях знающих чего хотят. А они могут адекватно судить, что им нужно.

     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2024 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру